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
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
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.