Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Instances For
def
Aesop.RuleBuilder.getCasesIndexingMode
(decl : Lean.Name)
(indexMd : Lean.Meta.TransparencyMode)
(casesPatterns : Array CasesPattern)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.RuleBuilder.casesCore
(info : Lean.InductiveVal)
(pats : Array CasesPattern)
(imode? : Option IndexingMode)
(md indexMd : Lean.Meta.TransparencyMode)
(phase : PhaseSpec)
:
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.