Documentation

Create an open term in the current context.

Create an open term which is closed.

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