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

Equations

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

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

Equations

• Aesop.CasesPattern.toIndexingMode p = Lean.withoutModifyingState do let __do_lift ← Aesop.CasesPattern.toExpr p Aesop.IndexingMode.hyps <$> Lean.Meta.DiscrTree.mkPath __do_lift

structure Aesop.CasesBuilderOptionsextends Aesop.RegularBuilderOptions : Type

• indexingMode? : Option Aesop.IndexingMode
• patterns : Array Aesop.CasesPattern
• transparency : Lean.Meta.TransparencyMode

  The transparency used by the rule tactic when searching for hypotheses to run cases on.

• indexTransparency : Lean.Meta.TransparencyMode

  The transparency used to index the rule. The rule is not indexed unless this is .reducible.

instance Aesop.CasesBuilderOptions.instInhabitedCasesBuilderOptions : Inhabited Aesop.CasesBuilderOptions

Equations

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

def Aesop.CasesBuilderOptions.indexingMode (decl : Lean.Name) (opts : Aesop.CasesBuilderOptions) : Lean.MetaM Aesop.IndexingMode

Equations

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

def Aesop.CasesBuilderOptions.target (decl : Lean.Name) (opts : Aesop.CasesBuilderOptions) : Aesop.CasesTarget

Equations

• Aesop.CasesBuilderOptions.target decl opts = if Array.isEmpty opts.patterns = true then Aesop.CasesTarget.decl decl else Aesop.CasesTarget.patterns opts.patterns

def Aesop.RuleBuilder.cases (opts : Aesop.CasesBuilderOptions) : Aesop.RuleBuilder

Equations

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

def Aesop.RuleBuilder.cases.name : Aesop.BuilderName

Equations

• Aesop.RuleBuilder.cases.name = Aesop.BuilderName.cases