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.instInhabitedIndexingMode.default }

def Aesop.instInhabitedIndexingMode.default : 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

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

inductive Aesop.IndexMatchLocation : Type

The source of a rule match reported by the index. We assume that only IndexMatchLocations belonging to the same goal are equated or compared.

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

instance Aesop.instInhabitedIndexMatchLocation : Inhabited IndexMatchLocation

Equations

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

def Aesop.instInhabitedIndexMatchLocation.default : 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

A rule that, according to the index, should be applied to the current goal. In addition to the rule, this data structure contains information about how the rule should be applied. For example, if the rule has rule patterns, we report the substitutions obtained by matching the rule patterns against the current goal.

• rule : α

  The rule that should be applied.

• locations : Array IndexMatchLocation

  Goal locations where the rule matched. The rule's indexingMode determines which locations can be contained in this set. The array contains no duplicates.

• patternSubsts? : Option (Array Substitution)

  Pattern substitutions for this rule that were found in the goal. none iff the rule doesn't have a pattern. The array contains no duplicates.

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

Equations

• Aesop.instInhabitedIndexMatchResult = { default := Aesop.instInhabitedIndexMatchResult.default }

def Aesop.instInhabitedIndexMatchResult.default {a✝ : Type} [Inhabited a✝] : 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 }