inductive Aesop.RawHyp : Type

A hypothesis that has not yet been matched against a premise, or a rule pattern substitution.

• fvarId (fvarId : Lean.FVarId) : RawHyp

  The hypothesis.

• patSubst (subst : Substitution) : RawHyp

  The rule pattern substitution.

def Aesop.instInhabitedRawHyp.default : RawHyp

Equations

• Aesop.instInhabitedRawHyp.default = Aesop.RawHyp.fvarId default

instance Aesop.instInhabitedRawHyp : Inhabited RawHyp

Equations

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

def Aesop.instBEqRawHyp.beq : RawHyp → RawHyp → Bool

Equations

• Aesop.instBEqRawHyp.beq (Aesop.RawHyp.fvarId a) (Aesop.RawHyp.fvarId b) = (a == b)
• Aesop.instBEqRawHyp.beq (Aesop.RawHyp.patSubst a) (Aesop.RawHyp.patSubst b) = (a == b)
• Aesop.instBEqRawHyp.beq x✝¹ x✝ = false

instance Aesop.instBEqRawHyp : BEq RawHyp

Equations

• Aesop.instBEqRawHyp = { beq := Aesop.instBEqRawHyp.beq }

instance Aesop.instHashableRawHyp : Hashable RawHyp

Equations

• Aesop.instHashableRawHyp = { hash := Aesop.instHashableRawHyp.hash }

def Aesop.instHashableRawHyp.hash : RawHyp → UInt64

Equations

• Aesop.instHashableRawHyp.hash (Aesop.RawHyp.fvarId a) = mixHash 0 (hash a)
• Aesop.instHashableRawHyp.hash (Aesop.RawHyp.patSubst a) = mixHash 1 (hash a)

instance Aesop.instToMessageDataRawHyp : Lean.ToMessageData RawHyp

Equations

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

structure Aesop.Hyp : Type

A hypothesis that was matched against a premise, or a rule pattern substitution.

• fvarId? : Option Lean.FVarId

  The hypothesis, or none if this is a rule pattern substitution.

• subst : Substitution

  The substitution that results from matching the hypothesis against a premise or that was derived from the pattern.

def Aesop.instInhabitedHyp.default : Hyp

Equations

• Aesop.instInhabitedHyp.default = { fvarId? := default, subst := default }

instance Aesop.instInhabitedHyp : Inhabited Hyp

Equations

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

instance Aesop.Hyp.instBEq : BEq Hyp

Equations

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

instance Aesop.Hyp.instHashable : Hashable Hyp

Equations

• Aesop.Hyp.instHashable = { hash := fun (h : Aesop.Hyp) => match h.fvarId? with | some h => hash h | none => hash h.subst }

def Aesop.Hyp.containsHyp (fvarId : Lean.FVarId) (h : Hyp) : Bool

Returns true if h is the hyp fvarId or is a pattern substitution containing fvarId.

Equations

• Aesop.Hyp.containsHyp fvarId h = (h.fvarId? == some fvarId || Aesop.Substitution.containsHyp fvarId h.subst)

def Aesop.Hyp.isPatSubst (h : Hyp) : Bool

Does this Hyp represent a pattern substitution?

Equations

• h.isPatSubst = h.fvarId?.isSome

structure Aesop.InstMap : Type

Partial matches associated with a particular slot instantiation. An entry s ↦ e ↦ (ms, hs) indicates that for the instantiation e of slot s, we have partial matches ms and hypotheses hs.

• map : Lean.PHashMap SlotIndex (EMap (Lean.PHashSet Match × Lean.PHashSet Hyp))

def Aesop.instInhabitedInstMap.default : InstMap

Equations

• Aesop.instInhabitedInstMap.default = { map := default }

instance Aesop.instInhabitedInstMap : Inhabited InstMap

Equations

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

instance Aesop.InstMap.instEmptyCollection : EmptyCollection InstMap

Equations

• Aesop.InstMap.instEmptyCollection = { emptyCollection := { map := Lean.PersistentHashMap.empty } }

instance Aesop.InstMap.instToMessageData : Lean.ToMessageData InstMap

Equations

• Aesop.InstMap.instToMessageData = { toMessageData := fun (m : Aesop.InstMap) => Aesop.InstMap.instToMessageData._private_1 m }

@[inline]

def Aesop.InstMap.find? (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) : Lean.MetaM (Option (Lean.PHashSet Match × Lean.PHashSet Hyp))

Returns the set of matches and hypotheses associated with a slot slot with instantiation inst.

Equations

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

@[inline]

def Aesop.InstMap.findD (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) : Lean.MetaM (Lean.PHashSet Match × Lean.PHashSet Hyp)

Returns the set of matches and hypotheses associated with a slot slot with instantiation inst, or (∅, ∅) if slot and inst do not have any associated matches.

Equations

• imap.findD slot inst = do let __do_lift ← imap.find? slot inst pure (__do_lift.getD (∅, ∅))

def Aesop.InstMap.modify {α : Type} (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) (f : Lean.PHashSet Match → Lean.PHashSet Hyp → Lean.PHashSet Match × Lean.PHashSet Hyp × α) : Lean.MetaM (InstMap × α)

Applies a transformation to the data associated with slot and inst. If there is no such data, the transformation is applied to (∅, ∅). Returns the new instantiation map and the result of f.

Equations

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

def Aesop.InstMap.insertHyp (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) (hyp : Hyp) : Lean.MetaM (InstMap × Bool)

Inserts a hyp associated with slot slot and instantiation inst. The hyp must be a valid assignment for the slot's premise. Returns true if the hyp was not previously associated with slot and inst.

Equations

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

def Aesop.InstMap.insertMatchCore (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) (m : Match) : Lean.MetaM (InstMap × Bool)

Inserts a match associated with slot slot and instantiation inst. The match's level must be slot. Returns true if the match was not previously associated with slot and inst.

Equations

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

def Aesop.InstMap.insertMatch (imap : InstMap) (var : PremiseIndex) (m : Match) : BaseM (InstMap × Bool)

Inserts a match. The match m is associated with the slot given by its level (i.e., the maximal slot for which m contains a hypothesis) and the instantiation of var given by the map's substitution. Returns true if the match was not previously associated with this slot and instantiation.

Equations

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

def Aesop.InstMap.modifyMapsForSlotsFrom (imap : InstMap) (slot : SlotIndex) (f : Lean.PHashSet Match → Lean.PHashSet Hyp → Lean.PHashSet Match × Lean.PHashSet Hyp) : InstMap

Modify the maps for slot slot and all later slots.

Equations

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

def Aesop.InstMap.eraseHyp (imap : InstMap) (hyp : Lean.FVarId) (slot : SlotIndex) : InstMap

Remove hyp from slot and all later slots. For each mapping s ↦ e ↦ (ms, hs) in imap, if s ≥ slot, then hyp is removed from hs and any matches containing hyp are removed from ms.

Equations

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

def Aesop.InstMap.erasePatSubst (imap : InstMap) (subst : Substitution) (slot : SlotIndex) : InstMap

Remove the pattern substitution subst from slot and all later slots. For each mapping s ↦ e ↦ (ms, hs) in imap, if s ≥ slot, then subst is removed from hs and any matches containing subst are removed from ms.

Equations

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

def Aesop.InstMap.stats (imap : InstMap) : Array ForwardInstantiationStats

Extract stats from an InstMap.

Equations

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

structure Aesop.VariableMap : Type

Map from variables to the matches and hypotheses of slots whose types contain the variables.

• map : Lean.PHashMap PremiseIndex InstMap

def Aesop.instInhabitedVariableMap.default : VariableMap

Equations

• Aesop.instInhabitedVariableMap.default = { map := default }

instance Aesop.instInhabitedVariableMap : Inhabited VariableMap

Equations

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

instance Aesop.VariableMap.instEmptyCollection : EmptyCollection VariableMap

Equations

• Aesop.VariableMap.instEmptyCollection = { emptyCollection := { map := Lean.PersistentHashMap.empty } }

instance Aesop.VariableMap.instToMessageData : Lean.ToMessageData VariableMap

Equations

• Aesop.VariableMap.instToMessageData = { toMessageData := fun (m : Aesop.VariableMap) => Aesop.VariableMap.instToMessageData._private_1 m }

def Aesop.VariableMap.find? (vmap : VariableMap) (var : PremiseIndex) : Option InstMap

Get the InstMap associated with a variable.

Equations

• vmap.find? var = Lean.PersistentHashMap.find? vmap.map var

def Aesop.VariableMap.find (vmap : VariableMap) (var : PremiseIndex) : InstMap

Get the InstMap associated with a variable, or an empty InstMap.

Equations

• vmap.find var = (vmap.find? var).getD ∅

def Aesop.VariableMap.modifyM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (vmap : VariableMap) (var : PremiseIndex) (f : InstMap → m (InstMap × α)) : m (VariableMap × α)

Modify the InstMap associated to variable var. If no such InstMap exists, the function f is applied to the empty InstMap and the result is associated with var. Returns the new variable map and the result of f.

Equations

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

def Aesop.VariableMap.modify {α : Type u_1} (vmap : VariableMap) (var : PremiseIndex) (f : InstMap → InstMap × α) : VariableMap × α

Modify the InstMap associated to variable var. If no such InstMap exists, the function f is applied to the empty InstMap and the result is associated with var. Returns the new variable map and the result of f.

Equations

• vmap.modify var f = vmap.modifyM var f

def Aesop.VariableMap.addHyp (vmap : VariableMap) (slot : Slot) (hyp : Hyp) : BaseM (VariableMap × Bool)

Add a hypothesis hyp. Precondition: hyp matches the premise of slot slot with substitution hyp.subst (and hence hyp.subst contains a mapping for each variable in slot.common). Returns true if the variable map changed.

Equations

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

def Aesop.VariableMap.addMatch (vmap : VariableMap) (nextSlot : Slot) (m : Match) : BaseM (VariableMap × Bool)

Add a match m. Precondition: nextSlot is the slot with index m.level + 1. Returns true if the variable map changed.

Equations

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

def Aesop.VariableMap.eraseHyp (vmap : VariableMap) (hyp : Lean.FVarId) (slot : SlotIndex) : VariableMap

Remove a hyp from slot and all later slots.

Equations

• vmap.eraseHyp hyp slot = { map := Lean.PersistentHashMap.map vmap.map fun (x : Aesop.InstMap) => x.eraseHyp hyp slot }

def Aesop.VariableMap.erasePatSubst (vmap : VariableMap) (subst : Substitution) (slot : SlotIndex) : VariableMap

Remove the pattern substitution subst from slot and all later slots.

Equations

• vmap.erasePatSubst subst slot = { map := Lean.PersistentHashMap.map vmap.map fun (x : Aesop.InstMap) => x.erasePatSubst subst slot }

def Aesop.VariableMap.findMatches (vmap : VariableMap) (slot : Slot) (subst : Substitution) : BaseM (Std.HashSet Match)

Find matches in slot slot - 1 whose substitutions are compatible with subst. Preconditions: slot.index is nonzero, slot.common is nonempty and each variable contained in slot.common is also contained in subst.

Equations

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

def Aesop.VariableMap.findHyps (vmap : VariableMap) (slot : Slot) (subst : Substitution) : BaseM (Std.HashSet Hyp)

Find hyps in slot whose substitutions are compatible with subst. Precondition: slot.common is nonempty and each variable contained in it is also contained in subst.

Equations

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

def Aesop.VariableMap.stats (vmap : VariableMap) : Array ForwardInstantiationStats

Extract stats from a VariableMap.

Equations

• vmap.stats = Lean.PersistentHashMap.foldl vmap.map (fun (acc : Array Aesop.ForwardInstantiationStats) (x : Aesop.PremiseIndex) (imap : Aesop.InstMap) => acc ++ imap.stats) #[]

structure Aesop.ClusterState : Type

Structure representing the state of a slot cluster. Updates are performed lazily: the enqueueRawHyp method enqueues a hyp or patten subst to be added to the state, and the update method must be used to actually make the corresponding changes and potentially generate new complete matches.

• slots : Array Slot

  The cluster's slots.

• conclusionDeps : Array PremiseIndex

  The premises that appear in the rule's conclusion. These are the same for all cluster states of a rule, but are stored here for convenience.

• variableMap : VariableMap

  The variable map for this cluster.

• completeMatches : Lean.PHashSet Match

  Complete matches for this cluster.

• haveHypForEachSlot : Bool

  This flag is true if all slotQueues are potentially nonempty. Before that point, we do not add any hyps to the variable maps since the rule cannot possibly produce a complete match.

• slotQueues : Array (Array RawHyp)

  Hypotheses or pattern substitutions that have been added to the cluster state, but have not yet been added to the variableMap.

• slotQueues_size : self.slotQueues.size = self.slots.size

  There is exactly one queue for each slot.

instance Aesop.ClusterState.instInhabited : Inhabited ClusterState

Equations

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

instance Aesop.ClusterState.instToMessageData : Lean.ToMessageData ClusterState

Equations

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

@[always_inline]

def Aesop.ClusterState.slot! (cs : ClusterState) (slot : SlotIndex) : Slot

Get the slot with the given index. Panic if the index is invalid.

Equations

• cs.slot! slot = cs.slots[slot.toNat]!

def Aesop.ClusterState.findSlot? (cs : ClusterState) (i : PremiseIndex) : Option Slot

Get the slot with the given premise index.

Equations

• cs.findSlot? i = Array.find? (fun (x : Aesop.Slot) => x.premiseIndex == i) cs.slots

def Aesop.ClusterState.matchPremise? (premises : Array Lean.MVarId) (lmvarIds : Array Lean.LMVarId) (cs : ClusterState) (slot : SlotIndex) (hyp : Lean.FVarId) : BaseM (Option Substitution)

Match hypothesis hyp against the slot with index slot in cs (which must be a valid index).

Equations

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

structure Aesop.ClusterState.AddM.Context : Type

Context for the AddM monad.

• premiseMVars : Array Lean.MVarId

  Metavariables for the premises of the rule for which a hyp or match is being added. When adding hyps, they are unified with these metavariables.

• premiseLMVars : Array Lean.LMVarId

  Metavariables for level parameters appearing in the rule's premises.

@[reducible, inline]

abbrev Aesop.ClusterState.AddM (α : Type) : Type

A monad for operations that add hyps or matches to a cluster state. The monad's state is an array of complete matches discovered while adding hyps/matches.

Equations

• Aesop.ClusterState.AddM = ReaderT Aesop.ClusterState.AddM.Context (StateRefT' IO.RealWorld (Array Aesop.Match) Aesop.BaseM)

def Aesop.ClusterState.AddM.run {α : Type} (premiseMVars : Array Lean.MVarId) (premiseLMVars : Array Lean.LMVarId) (x : AddM α) : BaseM (α × Array Match)

Run an AddM action.

Equations

• Aesop.ClusterState.AddM.run premiseMVars premiseLMVars x = (ReaderT.run x { premiseMVars := premiseMVars, premiseLMVars := premiseLMVars }).run #[]

partial def Aesop.ClusterState.addMatch (cs : ClusterState) (m : Match) : AddM ClusterState

Add a match to the cluster state.

partial def Aesop.ClusterState.addHyp (cs : ClusterState) (slot : Slot) (h : Hyp) : AddM ClusterState

Add a hypothesis to the cluster state. hyp.subst must be the substitution that results from applying h to slot.

partial def Aesop.ClusterState.addRawHyp (h : RawHyp) (slot : Slot) (cs : ClusterState) : AddM ClusterState

Add a hypothesis or pattern substitution to the cluster state.

partial def Aesop.ClusterState.addQueuedRawHyps (slot : Slot) (cs : ClusterState) : AddM ClusterState

Insert the raw hyps from slot's queue into the variable map.

def Aesop.ClusterState.enqueueRawHyp (h : RawHyp) (pi : PremiseIndex) (cs : ClusterState) : ClusterState

Add a hypothesis or pattern substitution to the queue for its slot.

Equations

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

def Aesop.ClusterState.eraseEnqueuedRawHyp (h : RawHyp) (slot : Slot) (cs : ClusterState) : ClusterState

Erase a RawHyp from the slot queue of the given slot.

Equations

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

def Aesop.ClusterState.eraseHyp (h : Lean.FVarId) (pi : PremiseIndex) (cs : ClusterState) : ClusterState

Erase a hypothesis from the cluster state's variable map.

Equations

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

def Aesop.ClusterState.erasePatSubst (subst : Substitution) (pi : PremiseIndex) (cs : ClusterState) : ClusterState

Erase a pattern substitution from the cluster state.

Equations

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

def Aesop.ClusterState.update (cs : ClusterState) : AddM ClusterState

Update a cluster change, adding any enqueued hypotheses. This may result in new complete matches.

Equations

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

def Aesop.ClusterState.stats (cs : ClusterState) : ForwardClusterStateStats

Extract stats from a ClusterState.

Equations

• cs.stats = { slots := cs.slots.size, instantiationStats := cs.variableMap.stats }

inductive Aesop.PatSubstSource : Type

The source of a pattern substitution. The same substitution can have multiple sources.

• hyp (fvarId : Lean.FVarId) : PatSubstSource

  The pattern substitution came from the given hypothesis.

• target : PatSubstSource

  The pattern substitution came from the goal's target.

def Aesop.instInhabitedPatSubstSource.default : PatSubstSource

Equations

• Aesop.instInhabitedPatSubstSource.default = Aesop.PatSubstSource.hyp default

instance Aesop.instInhabitedPatSubstSource : Inhabited PatSubstSource

Equations

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

def Aesop.instHashablePatSubstSource.hash : PatSubstSource → UInt64

Equations

• Aesop.instHashablePatSubstSource.hash (Aesop.PatSubstSource.hyp a) = mixHash 0 (hash a)
• Aesop.instHashablePatSubstSource.hash Aesop.PatSubstSource.target = 1

instance Aesop.instHashablePatSubstSource : Hashable PatSubstSource

Equations

• Aesop.instHashablePatSubstSource = { hash := Aesop.instHashablePatSubstSource.hash }

instance Aesop.instBEqPatSubstSource : BEq PatSubstSource

Equations

• Aesop.instBEqPatSubstSource = { beq := Aesop.instBEqPatSubstSource.beq }

def Aesop.instBEqPatSubstSource.beq : PatSubstSource → PatSubstSource → Bool

Equations

• Aesop.instBEqPatSubstSource.beq (Aesop.PatSubstSource.hyp a) (Aesop.PatSubstSource.hyp b) = (a == b)
• Aesop.instBEqPatSubstSource.beq Aesop.PatSubstSource.target Aesop.PatSubstSource.target = true
• Aesop.instBEqPatSubstSource.beq x✝¹ x✝ = false

structure Aesop.RuleState : Type

Forward state for one rule. Updates are lazy: when adding a hyp or pattern subst to the rule, it is initially only enqueued in the cluster states. The update method must be called to actually make the corresponding changes, which result in new complete matches for the rule.

• rule : ForwardRule

  The rule to which this state belongs.

• clusterStates : Array ClusterState

  States for each of the rule's slot clusters.

• patSubstSources : Lean.PHashMap Substitution (Lean.PHashSet PatSubstSource)

  The sources of all pattern substitutions present in the clusterStates. Invariant: each pattern substitution in the cluster states is associated with a nonempty set.

instance Aesop.instInhabitedRuleState : Inhabited RuleState

Equations

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

def Aesop.instInhabitedRuleState.default : RuleState

Equations

• Aesop.instInhabitedRuleState.default = { rule := default, clusterStates := default, patSubstSources := default }

instance Aesop.instToMessageDataRuleState : Lean.ToMessageData RuleState

Equations

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

def Aesop.ForwardRule.initialRuleState (r : ForwardRule) : RuleState

The initial (empty) rule state for a given forward rule.

Equations

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

def Aesop.RuleState.enqueueRawHyp (hyp : RawHyp) (pi : PremiseIndex) (rs : RuleState) : RuleState

Add a hypothesis or pattern substitution to the rule state. The hypothesis's type does not necessarily need to match the given premise. If it does not, this is detected by update and the hyp is not added.

Equations

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

def Aesop.RuleState.erasePatSubst (subst : Substitution) (source : PatSubstSource) (rs : RuleState) : RuleState

Erase a pattern substitution that was obtained from the given source.

Equations

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

def Aesop.RuleState.eraseHyp (h : Lean.FVarId) (pi : PremiseIndex) (rs : RuleState) : RuleState

Erase a hypothesis from the rule state.

Equations

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

def Aesop.RuleState.update (goal : Lean.MVarId) (rs : RuleState) : BaseM (RuleState × Array ForwardRuleMatch)

Add any enqueued hyps to the rule state, potentially generating new complete matches in the process.

Equations

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

def Aesop.RuleState.stats (rs : RuleState) : ForwardRuleStateStats

Extract stats from a RuleState.

Equations

• rs.stats = { ruleName := rs.rule.name, clusterStateStats := Array.map (fun (x : Aesop.ClusterState) => x.stats) rs.clusterStates }

structure Aesop.ForwardState : Type

State representing the non-complete matches of a given set of forward rules in a given local context.

• ruleStates : Lean.PHashMap RuleName RuleState

  Map from each rule's name to its RuleState

• hyps : Lean.PHashMap Lean.FVarId (Lean.PArray (RuleName × PremiseIndex))

  A map from hypotheses to the rules and premises that they matched against when they were initially added to the rule state. Invariant: the rule states in which a hypothesis h appear are exactly those identified by the rule names in hyps[h]. Furthermore, h only appears in slots with premise indices greater than or equal to those in hyps[h].

• patSubsts : Lean.PHashMap PatSubstSource (Lean.PArray (RuleName × Substitution))

  The pattern substitutions present in the rule states. Invariant: patSubsts maps the source s to a rule name r and pattern substitution i iff the rule state of r contains i with source s.

instance Aesop.instInhabitedForwardState : Inhabited ForwardState

Equations

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

def Aesop.instInhabitedForwardState.default : ForwardState

Equations

• Aesop.instInhabitedForwardState.default = { ruleStates := default, hyps := default, patSubsts := default }

instance Aesop.ForwardState.instEmptyCollection : EmptyCollection ForwardState

Equations

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

instance Aesop.ForwardState.instToMessageData : Lean.ToMessageData ForwardState

Equations

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

def Aesop.ForwardState.enqueueHyp (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (fs : ForwardState) : ForwardState

Add a hypothesis to the forward state. If fs represents a local context lctx, then fs.addHyp h ms represents lctx with h added. ms must overapproximate the rules for which h may unify with a maximal premise.

Equations

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

def Aesop.ForwardState.enqueuePatSubst (r : ForwardRule) (patSubst : Substitution) (source : PatSubstSource) (fs : ForwardState) : ForwardState

Add a pattern substitution to the forward state.

Equations

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

def Aesop.ForwardState.enqueuePatSubsts (source : PatSubstSource) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : ForwardState

Add multiple pattern substitutions to the forward state.

Equations

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

def Aesop.ForwardState.enqueueHypWithPatSubsts (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : ForwardState

Add a hypothesis and to the forward state, along with any rule pattern substitutions obtained from it.

Equations

• Aesop.ForwardState.enqueueHypWithPatSubsts h ms patSubsts fs = Aesop.ForwardState.enqueuePatSubsts (Aesop.PatSubstSource.hyp h) patSubsts (Aesop.ForwardState.enqueueHyp h ms fs)

def Aesop.ForwardState.erasePatSubsts (source : PatSubstSource) (fs : ForwardState) : ForwardState

Erase pattern substitutions with the given source.

Equations

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

def Aesop.ForwardState.eraseHyp (h : Lean.FVarId) (fs : ForwardState) : ForwardState

Remove a hypothesis from the forward state. If fs represents a local context lctx, then fs.eraseHyp h represents lctx with h removed.

Equations

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

def Aesop.ForwardState.eraseTargetPatSubsts (fs : ForwardState) : ForwardState

Erase all pattern substitutions whose source is the target.

Equations

• fs.eraseTargetPatSubsts = Aesop.ForwardState.erasePatSubsts Aesop.PatSubstSource.target fs

def Aesop.ForwardState.enqueueTargetPatSubsts (newPatSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : ForwardState

Update the pattern substitutions after the goal's target changed. goal is the new goal. newPatSubsts are the new target's pattern substitutions.

Equations

• Aesop.ForwardState.enqueueTargetPatSubsts newPatSubsts fs = Aesop.ForwardState.enqueuePatSubsts Aesop.PatSubstSource.target newPatSubsts fs.eraseTargetPatSubsts

def Aesop.ForwardState.update (goal : Lean.MVarId) (fs : ForwardState) (phase? : Option PhaseName) : BaseM (ForwardState × Array ForwardRuleMatch)

Update the forward state. This applies any previously enqueued changes to all rule states, potentially generating new complete matches in the process. If a phase is given, only rules from that phase are updated.

Equations

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

def Aesop.ForwardState.stats (fs : ForwardState) : ForwardStateStats

Extract stats from a ForwardState.

Equations

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