mathlib documentation

core / init.meta.type_context

meta constant tactic.unsafe.type_context  :
Type → Type

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.

meta constant tactic.unsafe.type_context.pure {α : Type} :

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.

meta constant tactic.unsafe.type_context.fold_mvars {α : Type} (f : α → exprtactic.unsafe.type_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

meta constant tactic.unsafe.type_context.tmp_mode {α : Type} (n_uvars n_mvars : ) :

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.

meta constant tactic.unsafe.type_context.mk_tmp_mvar (index : ) (type : expr) :

Return tt iff t "occurs" in e. The occurrence checking is performed using keyed matching with the given transparency setting.

We say t occurs in e by keyed matching iff there is a subterm s s.t. t and s have the same head, and is_def_eq t s md

The main idea is to minimize the number of is_def_eq checks performed.

Abstracts all occurrences of the term t in e using keyed matching. If unify is ff, then matching is used instead of unification. That is, metavariables occurring in e are not assigned.

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. [warning]: the local context modified by push_local and pop_local is not affected by try. 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