inductive Aesop.IndexingMode : Type

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

instance Aesop.instInhabitedIndexingMode : Inhabited IndexingMode

Equations

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

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

instance Aesop.IndexingMode.instToFormat : Std.ToFormat IndexingMode

Equations

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

def Aesop.IndexingMode.targetMatchingConclusion (type : Lean.Expr) : Lean.MetaM 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 IndexingMode

Equations

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

inductive Aesop.IndexMatchLocation : Type

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

instance Aesop.instInhabitedIndexMatchLocation : Inhabited IndexMatchLocation

Equations

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

instance Aesop.IndexMatchLocation.instToMessageData : Lean.ToMessageData IndexMatchLocation

Equations

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

instance Aesop.IndexMatchLocation.instBEq : BEq IndexMatchLocation

Equations

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

instance Aesop.IndexMatchLocation.instOrd : Ord IndexMatchLocation

Equations

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

instance Aesop.IndexMatchLocation.instHashable : Hashable IndexMatchLocation

Equations

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

structure Aesop.IndexMatchResult (α : Type) : Type

• rule : α
• locations : Std.HashSet IndexMatchLocation
• patternSubsts? : Option (Std.HashSet Substitution)

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

Equations

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

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

Equations

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

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

Equations

• Aesop.IndexMatchResult.instLTOfOrd = ltOfOrd

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

Equations

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