def Aesop.discrTreeConfig : Lean.Meta.ConfigWithKey

Equations

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

inductive Aesop.IndexingMode : Type

• unindexed : Aesop.IndexingMode
• target (keys : Array Lean.Meta.DiscrTree.Key) : Aesop.IndexingMode
• hyps (keys : Array Lean.Meta.DiscrTree.Key) : Aesop.IndexingMode
• or (imodes : Array Aesop.IndexingMode) : Aesop.IndexingMode

instance Aesop.instInhabitedIndexingMode : Inhabited Aesop.IndexingMode

Equations

• Aesop.instInhabitedIndexingMode = { default := Aesop.IndexingMode.unindexed }

partial def Aesop.IndexingMode.format : Aesop.IndexingMode → Lean.Format

instance Aesop.IndexingMode.instToFormat : Lean.ToFormat Aesop.IndexingMode

Equations

• Aesop.IndexingMode.instToFormat = { format := Aesop.IndexingMode.format }

def Aesop.IndexingMode.targetMatchingConclusion (type : Lean.Expr) : Lean.MetaM Aesop.IndexingMode

Equations

• Aesop.IndexingMode.targetMatchingConclusion type = do let path ← Aesop.getConclusionDiscrTreeKeys type pure (Aesop.IndexingMode.target path)

def Aesop.IndexingMode.hypsMatchingConst (decl : Lean.Name) : Lean.MetaM Aesop.IndexingMode

Equations

• Aesop.IndexingMode.hypsMatchingConst decl = do let path ← Aesop.getConstDiscrTreeKeys decl pure (Aesop.IndexingMode.hyps path)

inductive Aesop.IndexMatchLocation : Type

• none : Aesop.IndexMatchLocation
• target : Aesop.IndexMatchLocation
• hyp (ldecl : Lean.LocalDecl) : Aesop.IndexMatchLocation

instance Aesop.instInhabitedIndexMatchLocation : Inhabited Aesop.IndexMatchLocation

Equations

• Aesop.instInhabitedIndexMatchLocation = { default := Aesop.IndexMatchLocation.none }

instance Aesop.IndexMatchLocation.instToMessageData : Lean.ToMessageData Aesop.IndexMatchLocation

Equations

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

instance Aesop.IndexMatchLocation.instBEq : BEq Aesop.IndexMatchLocation

Equations

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

instance Aesop.IndexMatchLocation.instOrd : Ord Aesop.IndexMatchLocation

Equations

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

instance Aesop.IndexMatchLocation.instHashable : Hashable Aesop.IndexMatchLocation

Equations

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

structure Aesop.IndexMatchResult (α : Type) : Type

• rule : α
• locations : Std.HashSet Aesop.IndexMatchLocation
• patternInstantiations : Std.HashSet Aesop.RulePatternInstantiation

instance Aesop.instInhabitedIndexMatchResult {a✝ : Type} [Inhabited a✝] : Inhabited (Aesop.IndexMatchResult a✝)

Equations

• Aesop.instInhabitedIndexMatchResult = { default := { rule := default, locations := default, patternInstantiations := default } }

instance Aesop.IndexMatchResult.instOrd {α : Type} [Ord α] : Ord (Aesop.IndexMatchResult α)

Equations

• Aesop.IndexMatchResult.instOrd = { compare := fun (r s : Aesop.IndexMatchResult α) => compare r.rule s.rule }

instance Aesop.IndexMatchResult.instLTOfOrd {α : Type} [Ord α] : LT (Aesop.IndexMatchResult α)

Equations

• Aesop.IndexMatchResult.instLTOfOrd = ltOfOrd

instance Aesop.IndexMatchResult.instToMessageData {α : Type} [Lean.ToMessageData α] : Lean.ToMessageData (Aesop.IndexMatchResult α)

Equations

• Aesop.IndexMatchResult.instToMessageData = { toMessageData := fun (r : Aesop.IndexMatchResult α) => Lean.toMessageData r.rule }