Runs a term elaborator inside a tactic.
This function ensures that term elaboration fails when backtracking,
i.e., in first| tac term | other.
Instances For
Instances For
Elaborate stx in the current MVarContext. If given, the expectedType will be used to help
elaboration but not enforced (use elabTermEnsuringType to enforce an expected type).
Instances For
Elaborate stx in the current MVarContext. If given, the expectedType will be used to help
elaboration and then a TypeMismatchError will be thrown if the elaborated type doesn't match.
Instances For
Try to close main goal using x target, where target is the type of the main goal.
Instances For
Instances For
Instances For
Instances For
Instances For
Execute k, and collect new "holes" in the resulting expression.
Instances For
Instances For
Instances For
If allowNaturalHoles == true, then we allow the resultant expression to contain unassigned "natural" metavariables.
Recall that "natutal" metavariables are created for explicit holes _ and implicit arguments. They are meant to be
filled by typing constraints.
"Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation ?.
Instances For
Given a tactic
apply f
we want the apply tactic to create all metavariables. The following
definition will return @f for f. That is, it will not create
metavariables for implicit arguments.
A similar method is also used in Lean 3.
This method is useful when applying lemmas such as:
theorem infLeRight {s t : Set α} : s ⊓ t ≤ t
where s ≤ t here is defined as
∀ {x : α}, x ∈ s → x ∈ t
Instances For
Instances For
Instances For
Instances For
Elaborate stx. If it a free variable, return it. Otherwise, assert it, and return the free variable.
Note that, the main goal is updated when Meta.assert is used in the second case.