Compute the number of expected arguments and whether the result type is of the form (?m ...) where ?m is an unassigned metavariable.
Equations
- Lean.Meta.getExpectedNumArgsAux e = Lean.Meta.withDefault (Lean.Meta.forallTelescopeReducing e fun (xs : Array Lean.Expr) (body : Lean.Expr) => pure (xs.size, body.getAppFn.isMVar))
Instances For
Equations
- Lean.Meta.getExpectedNumArgs e = do let __discr ← Lean.Meta.getExpectedNumArgsAux e match __discr with | (numArgs, snd) => pure numArgs
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
If synthAssignedInstances
is true
, then apply
will synthesize instance implicit arguments
even if they have assigned by isDefEq
, and then check whether the synthesized value matches the
one inferred. The congr
tactic sets this flag to false.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Close the given goal using apply e
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.apply mvarId e cfg = mvarId.apply e cfg
Instances For
Short-hand for applying a constant to the goal.
Equations
- mvar.applyConst c cfg = do let __do_lift ← Lean.Meta.mkConstWithFreshMVarLevels c mvar.apply __do_lift cfg
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.splitAnd mvarId = mvarId.splitAnd
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply the n
-th constructor of the target type,
checking that it is an inductive type,
and that there are the expected number of constructors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try to convert an Iff
into an Eq
by applying iff_of_eq
.
If successful, returns the new goal, and otherwise returns the original MVarId
.
This may be regarded as being a special case of Lean.MVarId.liftReflToEq
, specifically for Iff
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try to close the goal using proof_irrel_heq
. Returns whether or not it succeeds.
We need to be somewhat careful not to assign metavariables while doing this, otherwise we might
specialize Sort _
to Prop
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try to close the goal using Subsingleton.elim
. Returns whether or not it succeeds.
We are careful to apply Subsingleton.elim
in a way that does not assign any metavariables.
This is to prevent the Subsingleton Prop
instance from being used as justification to specialize
Sort _
to Prop
.
Equations
- One or more equations did not get rendered due to their size.