A monad that exposes the functionality of the C++ class
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
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.
@has_add.add nat ?m a b can't project because
?m is not given.
Set the mvar to the following assignments.
Works for temporary metas too.
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
- It is not checked whether the assignment uses local constants outside the declaration's context.
You can avoid the unsafety by using
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.
Return tt iff
t "occurs" in
e. The occurrence checking is performed using
keyed matching with the given transparency setting.
t occurs in
e by keyed matching iff there is a subterm
s have the same head, and
is_def_eq t s md
The main idea is to minimize the number of
Abstracts all occurrences of the term
e using keyed matching.
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
pop_local is not affected by
Any unpopped locals will be present after the
try even if the inner
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.