Equations
- Lean.Elab.Tactic.isHoleRHS rhs = (rhs.isOfKind `Lean.Parser.Term.syntheticHole || rhs.isOfKind `Lean.Parser.Term.hole)
Instances For
Helper method for creating an user-defined eliminator/recursor application.
- name : Name
The short name of the alternative, used in
| foo =>
cases - info : Meta.ElimAltInfo
- mvarId : MVarId
The subgoal metavariable for the alternative.
Instances For
- elimInfo : Meta.ElimInfo
Instances For
Equations
Instances For
Construct the an eliminator/recursor application. targets
contains the explicit and implicit
targets for the eliminator, not yet generalized.
For example, the indices of builtin recursors are considered implicit targets.
Remark: the method addImplicitTargets
may be used to compute the sequence of implicit and
explicit targets from the explicit ones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a goal ... targets ... |- C[targets, complexArgs]
associated with mvarId
,
where complexArgs
are the the complex (i.e. non-target) arguments to the motive in the conclusion
of the eliminator, construct motiveArg := fun targets rs => C[targets, rs]
This checks if the type of the complex arguments match what's expected by the motive, and
ignores them otherwise. This limits the ability of cases
to use unfolding function
principles with dependent types, because after generalization of the targets, the types do
no longer match. This can likely be improved.
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
- 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
Applies syntactic alternative to alternative goal.
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
Interprets a Lean.Parser.Tactic.elimTarget
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Elaborates the targets (Lean.Parser.Tactic.elimTarget
),
generalizing them if requested or if otherwise necessary.
Returns
- the targets as fvars and
- an array of identifier/fvarid pairs so that the
induction
/cases
tactic can annotate any user-supplied target hypothesis names usingTerm.addLocalVarInfo
.
Modifies the current goal when generalizing.
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
- One or more equations did not get rendered due to their size.
Instances For
The code path shared between cases
and fun_cases
; when we already have an elimInfo
and the targets
contains the implicit targets
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
- One or more equations did not get rendered due to their size.