Documentation

Create an open term in the current context.

Create an open term which is closed.

Check if an Open is closed.

Extract the value from an open term. Must be done in an extension of the context in which the term was created.

Try to use an Open the current context. Returns Nothing if current context is not an extension of the context in which the Open was created.