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.

instance Aesop.instInhabitedRawHyp : Inhabited RawHyp

Equations

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

instance Aesop.instBEqRawHyp : BEq RawHyp

Equations

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

instance Aesop.instHashableRawHyp : Hashable RawHyp

Equations

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

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.

instance Aesop.instInhabitedHyp : Inhabited Hyp

Equations

• Aesop.instInhabitedHyp = { default := { fvarId? := default, subst := 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 (Lean.PHashMap RPINF (Lean.PHashSet Match × Lean.PHashSet Hyp))

instance Aesop.instInhabitedInstMap : Inhabited InstMap

Equations

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

instance Aesop.InstMap.instEmptyCollection : EmptyCollection InstMap

Equations

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

instance Aesop.InstMap.instToMessageData : Lean.ToMessageData InstMap

Equations

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

@[inline]

def Aesop.InstMap.find? (imap : InstMap) (slot : SlotIndex) (inst : RPINF) : 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 : RPINF) : 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 = (imap.find? slot inst).getD (∅, ∅)

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

Applies a transfomation to the data associated to 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 : RPINF) (hyp : Hyp) : 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 : RPINF) (m : Match) : 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) : 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.

structure Aesop.VariableMap : Type

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

• map : Lean.PHashMap PremiseIndex InstMap

instance Aesop.instInhabitedVariableMap : Inhabited VariableMap

Equations

• Aesop.instInhabitedVariableMap = { default := { map := 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.ppPHashMap✝ true m.map }

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.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

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

def Aesop.VariableMap.addHyp (vmap : VariableMap) (slot : Slot) (hyp : Hyp) : 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) : 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) : 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.findMatches.prevSlotMatches (vmap : VariableMap) (slot : Slot) (subst : Substitution) (var : PremiseIndex) : Lean.PHashSet Match

Equations

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

def Aesop.VariableMap.findHyps (vmap : VariableMap) (slot : Slot) (subst : Substitution) : 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.findHyps.slotHyps (vmap : VariableMap) (slot : Slot) (subst : Substitution) (var : PremiseIndex) : Lean.PHashSet Hyp

Equations

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

structure Aesop.ClusterState : Type

Structure representing the state of a slot cluster.

• 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.

• addHypsLazily : Bool

  When this flag is true, hyps are added to the slotQueues rather than the variableMap. This is an optimisation that avoids performing unifications until a rule can potentially generate a complete match. More precisely:

  • addHypsLazily is initially set to true.
  • While addHypsLazily is true, hyps are added to (and deleted from) the slotQueues and are not added to the variableMap. Once an addition causes all slot queues to have at least one element, addHypsLazily is permanently set to false and hyps for slot 0 are added to the variableMap.
  • While addHypsLazily is false:
    • Hyps for slot i are added directly to the variable maps if i = 0 or the slot i - 1 has matches. Otherwise they are added to the slot queue for i. (More precisely, we only track whether slot i - 1 has had matches at some point. This allows us to ignore deletions.)
    • The insertion of a match into slot i causes all hyps at slot i + 1 to be moved from the slot queue into the variableMap.
• 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.

• slotMaybeHasMatches : Array Bool

  The ith element of this array is true if a match was at some point added to slot i.

• slotMaybeHasMatches_size : self.slotMaybeHasMatches.size = self.slots.size

  There is exactly one boolean 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.

def Aesop.ClusterState.matchPremise?.updateSubst (hyp : Lean.FVarId) (premises : Array Lean.MVarId) (var : PremiseIndex) (subst : Substitution) : BaseM Substitution

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. Returns the new cluster state and any new complete matches for this cluster.

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.addRawHypCore (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) (slot : Slot) (cs : ClusterState) : ClusterState

Add a hypothesis or pattern substitution to the queue for its slot. If afterwards each slot queue contains at least one element, then the returned cluster state cs has cs.addHypsLazily = false.

Equations

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

def Aesop.ClusterState.addRawHyp (cs : ClusterState) (i : PremiseIndex) (h : RawHyp) : AddM ClusterState

Add a hypothesis or pattern substitution to the cluster state. If a hypothesis is given and its type does not match the premise corresponding to slot, it is not added.

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.

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.

instance Aesop.instInhabitedPatSubstSource : Inhabited PatSubstSource

Equations

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

instance Aesop.instHashablePatSubstSource : Hashable PatSubstSource

Equations

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

instance Aesop.instBEqPatSubstSource : BEq PatSubstSource

Equations

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

structure Aesop.RuleState : Type

Forward state for one 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 := { 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.addRawHyp (goal : Lean.MVarId) (h : RawHyp) (pi : PremiseIndex) (rs : RuleState) : BaseM (RuleState × Array CompleteMatch)

Add a hypothesis or pattern substitution to the rule state. Returns the new rule state and any newly completed matches. If a hypothesis is given and it does not match premise pi, nothing happens.

Equations

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

def Aesop.RuleState.addRawHyp.getCompleteMatches (clusterStates : Array ClusterState) (clusterIdx : Nat) (newCompleteMatches : Array Match) : Array CompleteMatch

Equations

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

def Aesop.RuleState.addRawHyp.addMatches (completeMatches : Array CompleteMatch) (clusterMatches : Array Match) : Array CompleteMatch

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.

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.

• hypTypes : Lean.PHashSet RPINF

  Normalised types of all non-implementation detail hypotheses in the local context.

instance Aesop.instInhabitedForwardState : Inhabited ForwardState

Equations

• Aesop.instInhabitedForwardState = { default := { ruleStates := default, hyps := default, patSubsts := default, hypTypes := 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.addHypCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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.addHyp (goal : Lean.MVarId) (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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

• Aesop.ForwardState.addHyp goal h ms fs = Aesop.ForwardState.addHypCore #[] goal h ms fs

def Aesop.ForwardState.addPatSubstCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (r : ForwardRule) (patSubst : Substitution) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

Add a pattern substitution to the forward state.

Equations

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

def Aesop.ForwardState.addPatSubst (goal : Lean.MVarId) (r : ForwardRule) (patSubst : Substitution) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

Add a pattern substitution to the forward state.

Equations

• Aesop.ForwardState.addPatSubst goal r patSubst fs = Aesop.ForwardState.addPatSubstCore #[] goal r patSubst fs

def Aesop.ForwardState.addPatSubstsCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

Add multiple pattern substitutions to the forward state.

Equations

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

def Aesop.ForwardState.addPatSubsts (goal : Lean.MVarId) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

Add multiple pattern substitutions to the forward state.

Equations

• Aesop.ForwardState.addPatSubsts goal patSubsts fs = Aesop.ForwardState.addPatSubstsCore #[] goal patSubsts fs

def Aesop.ForwardState.addHypWithPatSubstsCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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

Equations

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

def Aesop.ForwardState.addHypWithPatSubsts (goal : Lean.MVarId) (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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

Equations

• Aesop.ForwardState.addHypWithPatSubsts goal h ms patSubsts fs = Aesop.ForwardState.addHypWithPatSubstsCore #[] goal h ms patSubsts 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) (type : RPINF) (fs : ForwardState) : ForwardState

Remove a hypothesis from the forward state. If fs represents a local context lctx, then fs.eraseHyp h ms represents lctx with h removed. type must be the normalised type of h. ms must contain all 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.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.updateTargetPatSubstsCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (newPatSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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.updateTargetPatSubstsCore ruleMatches goal newPatSubsts fs = Aesop.ForwardState.addPatSubstsCore ruleMatches goal newPatSubsts fs.eraseTargetPatSubsts

def Aesop.ForwardState.updateTargetPatSubsts (goal : Lean.MVarId) (newPatSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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.updateTargetPatSubsts goal newPatSubsts fs = Aesop.ForwardState.updateTargetPatSubstsCore #[] goal newPatSubsts fs