mathlib documentation

For simple and constructor vm_obj's, it returns the constructor tag/index. Return 0 otherwise.

For closure vm_obj's, it returns the internal function index.

For constructor vm_obj's, it returns the data stored in the object. For closure vm_obj's, it returns the local arguments captured by the closure.

For simple and mpz vm_obj's

For name vm_obj's, it returns the name wrapped by the vm_obj.

For level vm_obj's, it returns the universe level wrapped by the vm_obj.

For expr vm_obj's, it returns the expression wrapped by the vm_obj.

For declaration vm_obj's, it returns the declaration wrapped by the vm_obj.

For environment vm_obj's, it returns the environment wrapped by the vm_obj.

For tactic_state vm_obj's, it returns the tactic_state object wrapped by the vm_obj.

For format vm_obj's, it returns the format object wrapped by the vm_obj.

Internal function index associated with the given VM declaration.

Number of arguments needed to execute the given VM declaration.

Return source position if available

Return .olean file where the given VM declaration was imported from.

Return names .olean file where the given VM declaration was imported from.

If the given declaration is overridden by another declaration using the vm_override attribute, then this returns the overriding declaration.

Returns the vm declaration associated with the given name. Remark: does _not_ return the vm_override if present.

Returns the vm declaration associated with the given index. Remark: does _not_ return the vm_override if present.

Return the vm_obj stored at the given position on the execution stack. It fails if position >= vm.stack_size

Return (name, type) for the object at the given position on the execution stack. It fails if position >= vm.stack_size. The name is anonymous if vm_obj is a transient value created by the compiler. Type information is only recorded if the type is a closed term at compilation time.

Pretty print the vm_obj at the given position on the execution stack.

Pretty print the given expression.

Number of frames on the call stack.

Return the function name at the given stack frame. Action fails if position >= vm.call_stack_size.

Return the range [start, end) for the given stack frame. Action fails if position >= vm.call_stack_size. The values start and end correspond to positions at the execution stack. We have that 0 <= start < end <= vm.stack_size

Return the name of the function on top of the call stack.

Return the base stack pointer for the frame on top of the call stack.

Return the program counter.

Convert the given vm_obj into a string

Return tt if end of the input stream has been reached. For example, this can happen if the user presses Ctrl-D

Return the list of declarations tagged with the given attribute.