def Aesop.CasesPattern.check (decl : Lean.Name) (p : CasesPattern) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def Aesop.CasesPattern.toIndexingMode (p : CasesPattern) : Lean.MetaM IndexingMode

Equations

• p.toIndexingMode = Lean.withoutModifyingState do let __do_lift ← p.toExpr Aesop.IndexingMode.hyps <$> Aesop.mkDiscrTreePath __do_lift

def Aesop.RuleBuilderOptions.casesTransparency (opts : RuleBuilderOptions) : Lean.Meta.TransparencyMode

Equations

• opts.casesTransparency = opts.transparency?.getD Lean.Meta.TransparencyMode.reducible

def Aesop.RuleBuilderOptions.casesIndexTransparency (opts : RuleBuilderOptions) : Lean.Meta.TransparencyMode

Equations

• opts.casesIndexTransparency = opts.indexTransparency?.getD Lean.Meta.TransparencyMode.reducible

def Aesop.RuleBuilderOptions.casesPatterns (opts : RuleBuilderOptions) : Array CasesPattern

Equations

• opts.casesPatterns = opts.casesPatterns?.getD #[]

def Aesop.RuleBuilder.mkCasesTarget (decl : Lean.Name) (casesPatterns : Array CasesPattern) : CasesTarget

Equations

• Aesop.RuleBuilder.mkCasesTarget decl casesPatterns = if casesPatterns.isEmpty = true then Aesop.CasesTarget.decl decl else Aesop.CasesTarget.patterns casesPatterns

def Aesop.RuleBuilder.getCasesIndexingMode (decl : Lean.Name) (indexMd : Lean.Meta.TransparencyMode) (casesPatterns : Array CasesPattern) : Lean.MetaM IndexingMode

Equations

• One or more equations did not get rendered due to their size.

def Aesop.RuleBuilder.casesCore (info : Lean.InductiveVal) (pats : Array CasesPattern) (imode? : Option IndexingMode) (md indexMd : Lean.Meta.TransparencyMode) (phase : PhaseSpec) : Lean.MetaM LocalRuleSetMember

Equations

• One or more equations did not get rendered due to their size.

def Aesop.RuleBuilder.cases : RuleBuilder

Equations

• One or more equations did not get rendered due to their size.