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

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 : Std.HashSet IndexMatchLocation

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

• patternSubsts? : Option (Std.HashSet Substitution)

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

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 }