We use this method to report typeclass (and coercion) resolution problems that are "stuck". That is, there is nothing else to do, and we don't have enough information to synthesize them using TC resolution.
Instances For
Try to synthesize a term val
using the tactic code tacticCode
, and then assign mvarId := val
.
Try to process pending synthetic metavariables. If mayPostpone == false
,
then pendingMVars
is []
after executing this method.
It keeps executing synthesizeSyntheticMVarsStep
while progress is being made.
If mayPostpone == false
, then it applies default instances to SyntheticMVarKind.typeClass
(if available)
metavariables that are still unresolved, and then tries to resolve metavariables
with mayPostpone == false
. That is, we force them to produce error messages and/or commit to
a "best option". If, after that, we still haven't made progress, we report "stuck" errors.
Remark: we set ignoreStuckTC := true
when elaborating simp
arguments. Then,
pending TC problems become implicit parameters for the simp theorem.
Instances For
Instances For
Execute k
, and synthesize pending synthetic metavariables created while executing k
are solved.
If mayPostpone == false
, then all of them must be synthesized.
Remark: even if mayPostpone == true
, the method still uses synthesizeUsingDefault
Instances For
Similar to withSynthesize
, but sets mayPostpone
to true
, and do not use synthesizeUsingDefault
Instances For
Elaborate stx
, and make sure all pending synthetic metavariables created while elaborating stx
are solved.
Instances For
Collect unassigned metavariables at e
that have associated tactic blocks, and then execute them using runTactic
.
We use this method at the match .. with
elaborator when it cannot be postponed anymore, but it is still waiting
the result of a tactic block.