Documentation

Aesop.Index.Basic

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 :

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

Instances For

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 :

none: Aesop.IndexMatchLocation
target: Aesop.IndexMatchLocation
hyp: Lean.LocalDecl → Aesop.IndexMatchLocation

Instances For

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) :

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

Instances For

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 }