def Aesop.discrTreeConfig : Lean.Meta.WhnfCoreConfig

Equations

• Aesop.discrTreeConfig = { iota := false, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }

inductive Aesop.IndexingMode : Type

• unindexed: Aesop.IndexingMode
• target: Array Lean.Meta.DiscrTree.Key → Aesop.IndexingMode
• hyps: Array Lean.Meta.DiscrTree.Key → Aesop.IndexingMode
• or: 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 Aesop.discrTreeConfig 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: 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 : Lean.HashSet Aesop.IndexMatchLocation
• patternInstantiations : Lean.HashSet Aesop.RulePatternInstantiation

instance Aesop.instInhabitedIndexMatchResult : {a : Type} → [inst : 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 }