- fvarId : FVarId
- val : InductiveVal
Instances For
- allConsts : Std.HashSet Name
All constant symbols occurring in the gal.
- unfoldCandidates : Std.HashSet Name
Unfolding candiates.
- eqnCandidates : Std.HashSet Name
Equation function candiates.
- funIndCandidates : Std.HashSet FunIndCandidate
Function induction candidates.
- indCandidates : Array InductionCandidate
Induction candidates.
- libSearchResults : Std.HashSet (Name × Grind.EMatchTheoremKind)
Relevant declarations by
libSearch
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- Lean.Meta.Try.Collector.getConfig = do let __do_lift ← read pure __do_lift.config
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if declName
is in the module being compiled.
Equations
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
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
@[reducible, inline]
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
@[reducible, inline]