Returns a fresh copy of the current environment.

Set environment.

Term scope in the current environment.

Calls the continuation in the provided environment. Previous environment is restored after return.

Calls the continuation in a local copy of the environment. Previous environment is restored after return, but allocators are left unchanged to enforce on-the-fly alpha-conversion.

Calls the continuation in a fresh local environment. Previous environment is restored after return.

For Z->a arrays

For k->a arrays

Type variables.

Without parentheses.

With parentheses if non-atomic.

Calls the continuation with given mode for sub-terms. The englobing mode is passed to continuation and then restored.

Optional scoping post-fix operator when entering arithmetic mode.

"true"

"false"

Defaults to self#op_minus or self#op_mul

Constant array "[v...]".

Access "a[k]".

Update "a[k <- v]".

Field access.

Record construction.

Sub-terms that require parentheses. Shared sub-terms are detected on behalf of this method.

Printer with shared sub-terms printed with their name and without parentheses.

Printer with shared sub-terms printed with their name and within parentheses for non-atomic expressions. Additional scope terminates the expression when required (typically for Coq).

Raw representation of a term, as it is. This is where you should hook a printer to keep sharing, parentheses, and such.

Prints in term mode. Default uses self#pp_shared with mode Mterm inside an <hov> box.

Prints in prop mode. Default uses self#pp_shared with mode Mprop inside an <hv> box.

Prints in term, arithmetic or prop mode with respect to provided type.

Prints in term, arithmetic or prop mode with respect to the sort of term. Boolean expression that also have a property form are printed in Mprop mode.