Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- p.toIndexingMode = Lean.withoutModifyingState do let __do_lift ← p.toExpr Aesop.IndexingMode.hyps <$> Lean.Meta.DiscrTree.mkPath __do_lift Aesop.discrTreeConfig
Instances For
Equations
- opts.casesTransparency = opts.transparency?.getD Lean.Meta.TransparencyMode.reducible
Instances For
Equations
- opts.casesIndexTransparency = opts.indexTransparency?.getD Lean.Meta.TransparencyMode.reducible
Instances For
Equations
- opts.casesPatterns = opts.casesPatterns?.getD #[]
Instances For
def
Aesop.RuleBuilderOptions.casesIndexingMode
(decl : Lean.Name)
(opts : Aesop.RuleBuilderOptions)
:
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.