mathlib3 documentation

core / init.meta.type_context

meta constant tactic.unsafe.type_context :

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.

Instances for tactic.unsafe.type_context

@[protected]

meta constant tactic.unsafe.type_context.bind {α β : Type} :

tactic.unsafe.type_context α → (α → tactic.unsafe.type_context β) → tactic.unsafe.type_context β

@[protected]

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

α → tactic.unsafe.type_context α

@[protected]

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

format → tactic.unsafe.type_context α

@[protected]

meta def tactic.unsafe.type_context.failure {α : Type} :

tactic.unsafe.type_context α

@[protected, instance]

meta def tactic.unsafe.type_context.monad :

monad tactic.unsafe.type_context

@[protected, instance]

meta def tactic.unsafe.type_context.monad_fail :

monad_fail tactic.unsafe.type_context

meta constant tactic.unsafe.type_context.get_env :

tactic.unsafe.type_context environment

meta constant tactic.unsafe.type_context.whnf :

expr → tactic.unsafe.type_context expr

meta constant tactic.unsafe.type_context.is_def_eq (e₁ e₂ : expr) (approx : bool := bool.ff) :

tactic.unsafe.type_context bool

meta constant tactic.unsafe.type_context.unify (e₁ e₂ : expr) (approx : bool := bool.ff) :

tactic.unsafe.type_context bool

meta constant tactic.unsafe.type_context.infer :

expr → tactic.unsafe.type_context expr

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

meta constant tactic.unsafe.type_context.is_stuck :

expr → tactic.unsafe.type_context (option expr)

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.

meta constant tactic.unsafe.type_context.push_local (pp_name : name) (type : expr) (bi : binder_info := binder_info.default) :

tactic.unsafe.type_context expr

Add a local to the tc local context.

meta constant tactic.unsafe.type_context.pop_local :

tactic.unsafe.type_context unit

meta constant tactic.unsafe.type_context.get_local_context :

tactic.unsafe.type_context local_context

Get the local context of the type_context.

meta constant tactic.unsafe.type_context.mk_mvar (pp_name : name) (type : expr) (context : option local_context := option.none) :

tactic.unsafe.type_context expr

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 : α → expr → tactic.unsafe.type_context α) :

α → tactic.unsafe.type_context α

Iterate over all mvars in the mvar context.

meta def tactic.unsafe.type_context.list_mvars :

tactic.unsafe.type_context (list expr)

meta constant tactic.unsafe.type_context.assign (mvar assignment : expr) :

tactic.unsafe.type_context unit

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.

meta constant tactic.unsafe.type_context.level.assign (mvar assignment : level) :

tactic.unsafe.type_context unit

Assigns a given level metavariable.

meta constant tactic.unsafe.type_context.is_declared (e : expr) :

tactic.unsafe.type_context bool

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

meta constant tactic.unsafe.type_context.is_assigned (mvar : expr) :

tactic.unsafe.type_context bool

meta constant tactic.unsafe.type_context.get_context (mvar : expr) :

tactic.unsafe.type_context local_context

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

meta constant tactic.unsafe.type_context.get_assignment (mvar : expr) :

tactic.unsafe.type_context expr

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

meta constant tactic.unsafe.type_context.instantiate_mvars :

expr → tactic.unsafe.type_context expr

meta constant tactic.unsafe.type_context.level.instantiate_mvars :

level → tactic.unsafe.type_context level

meta constant tactic.unsafe.type_context.is_tmp_mvar (mvar : expr) :

tactic.unsafe.type_context bool

meta constant tactic.unsafe.type_context.is_regular_mvar (mvar : expr) :

tactic.unsafe.type_context bool

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

tactic.unsafe.type_context α → tactic.unsafe.type_context α

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.

meta constant tactic.unsafe.type_context.in_tmp_mode :

tactic.unsafe.type_context bool

Returns true when in temp mode.

meta constant tactic.unsafe.type_context.tmp_is_assigned :

ℕ → tactic.unsafe.type_context bool

meta constant tactic.unsafe.type_context.tmp_get_assignment :

ℕ → tactic.unsafe.type_context expr

meta constant tactic.unsafe.type_context.level.tmp_is_assigned :

ℕ → tactic.unsafe.type_context bool

meta constant tactic.unsafe.type_context.level.tmp_get_assignment :

ℕ → tactic.unsafe.type_context level

meta constant tactic.unsafe.type_context.to_tmp_mvars :

expr → tactic.unsafe.type_context (expr × list level × list expr)

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

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

meta constant tactic.unsafe.type_context.level.mk_tmp_mvar (index : ℕ) :

meta constant tactic.unsafe.type_context.kdepends_on (e t : expr) :

tactic.unsafe.type_context bool

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.

meta constant tactic.unsafe.type_context.kabstract (e t : expr) (unify : bool := bool.tt) :

tactic.unsafe.type_context expr

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.

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

tactic.unsafe.type_context α → tactic.unsafe.type_context (option α)

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.

meta def tactic.unsafe.type_context.orelse {α : Type} :

tactic.unsafe.type_context α → tactic.unsafe.type_context α → tactic.unsafe.type_context α

@[protected, instance]

meta def tactic.unsafe.type_context.type_context_alternative :

alternative tactic.unsafe.type_context

meta constant tactic.unsafe.type_context.run {α : Type} (inner : tactic.unsafe.type_context α) (tr : tactic.transparency := tactic.transparency.semireducible) :

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.

meta def tactic.unsafe.type_context.trace {α : Type u_1} [has_to_format α] :

α → tactic.unsafe.type_context unit

meta def tactic.unsafe.type_context.print_mvars :

tactic.unsafe.type_context unit

meta constant tactic.unsafe.type_context.get_fun_info (f : expr) (nargs : option ℕ := option.none) :

tactic.unsafe.type_context fun_info

Same as tactic.get_fun_info