mathlib documentation

A monad that exposes the functionality of the C++ class type_context_old. The idea is that the methods to type_context are more powerful but _unsafe_ in the sense that you can create terms that do not typecheck or that are infinitely descending. Under the hood, type_context is implemented as a reader monad, with a mutable type_context object.

Infer the type of the given expr. Inferring the type does not mean that it typechecks. Will fail if type can't be inferred.

A stuck expression e is an expression that _would_ reduce, except that a metavariable is present that prevents the reduction. Returns the metavariable which is causing the stuckage. For example, @has_add.add nat ?m a b can't project because ?m is not given.

Add a local to the tc local context.

Get the local context of the type_context.

Create and declare a new metavariable. If the local context is not given then it will use the current local context.

Iterate over all mvars in the mvar context.

Set the mvar to the following assignments. Works for temporary metas too. [WARNING] assign does not perform certain checks:

• No typecheck is done before assignment.
• If the metavariable is already assigned this will clobber the assignment.
• It will not stop you from assigning an metavariable to itself or creating cycles of metavariable assignments. These will manifest as 'deep recursion' exceptions when instantiate_mvars is used.
• It is not checked whether the assignment uses local constants outside the declaration's context.

You can avoid the unsafety by using unify instead.

Assigns a given level metavariable.

Returns true if the given expression is a declared local constant or a declared metavariable.

Given a metavariable, returns the local context that the metavariable was declared with.

Get the expression that is assigned to the given mvar expression. Fails if given a

Run the given type_context monad in a temporary mvar scope. Doing this twice will push the old tmp_mvar assignments to a stack. So it is safe to do this whether or not you are already in tmp mode.

Returns true when in temp mode.

Replace each metavariable in the given expression with a temporary metavariable.

Run the provided type_context within a backtracking scope. This means that any changes to the metavariable context will not be committed if the inner monad fails. Any unpopped locals will be present after the try even if the inner type_context failed.

Runs the given type_context monad using the type context of the current tactic state. You can use this to perform unsafe operations such as direct metavariable assignment and the use of temporary metavariables.

Same as tactic.get_fun_info