structure Aesop.ForwardRuleMatches : Type

Sets of complete matches for norm/safe/unsafe rules.

• normMatches : Lean.PHashSet ForwardRuleMatch

  Complete matches of norm rules.

• safeMatches : Lean.PHashSet ForwardRuleMatch

  Complete matches of safe rules.

• unsafeMatches : Lean.PHashSet ForwardRuleMatch

  Complete matches of unsafe rules.

def Aesop.instInhabitedForwardRuleMatches.default : ForwardRuleMatches

Equations

• Aesop.instInhabitedForwardRuleMatches.default = { normMatches := default, safeMatches := default, unsafeMatches := default }

@[implicit_reducible]

instance Aesop.instInhabitedForwardRuleMatches : Inhabited ForwardRuleMatches

Equations

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

def Aesop.ForwardRuleMatches.empty : ForwardRuleMatches

Empty ForwardRuleMatches.

Equations

• Aesop.ForwardRuleMatches.empty = { normMatches := ∅, safeMatches := ∅, unsafeMatches := ∅ }

@[implicit_reducible]

instance Aesop.ForwardRuleMatches.instEmptyCollection : EmptyCollection ForwardRuleMatches

Equations

• Aesop.ForwardRuleMatches.instEmptyCollection = { emptyCollection := Aesop.ForwardRuleMatches.empty }

def Aesop.ForwardRuleMatches.insert (m : ForwardRuleMatch) (ms : ForwardRuleMatches) : ForwardRuleMatches

Add a complete match.

Equations

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

def Aesop.ForwardRuleMatches.insertMany (ms : Array ForwardRuleMatch) (ms' : ForwardRuleMatches) : ForwardRuleMatches

Add several complete matches.

Equations

• Aesop.ForwardRuleMatches.insertMany ms ms' = Array.foldl (fun (ms' : Aesop.ForwardRuleMatches) (m : Aesop.ForwardRuleMatch) => Aesop.ForwardRuleMatches.insert m ms') ms' ms

def Aesop.ForwardRuleMatches.erase (m : ForwardRuleMatch) (ms : ForwardRuleMatches) : ForwardRuleMatches

Erase a complete match.

Equations

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

def Aesop.ForwardRuleMatches.eraseMany (ms : Array ForwardRuleMatch) (ms' : ForwardRuleMatches) : ForwardRuleMatches

Erase several complete matches.

Equations

• Aesop.ForwardRuleMatches.eraseMany ms ms' = Array.foldl (fun (ms' : Aesop.ForwardRuleMatches) (m : Aesop.ForwardRuleMatch) => Aesop.ForwardRuleMatches.erase m ms') ms' ms

def Aesop.ForwardRuleMatches.ofArray (ms : Array ForwardRuleMatch) : ForwardRuleMatches

Build a ForwardRuleMatches structure containing the matches from ms.

Equations

• Aesop.ForwardRuleMatches.ofArray ms = Aesop.ForwardRuleMatches.insertMany ms ∅

def Aesop.ForwardRuleMatches.eraseHyps (hs : Std.HashSet Lean.FVarId) (ms : ForwardRuleMatches) : ForwardRuleMatches

Erase matches containing any of the hypotheses hs from ms.

Equations

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

def Aesop.ForwardRuleMatches.eraseHyp (h : Lean.FVarId) (ms : ForwardRuleMatches) : ForwardRuleMatches

Erase matches containing the hypothesis h from ms.

Equations

• Aesop.ForwardRuleMatches.eraseHyp h ms = Aesop.ForwardRuleMatches.eraseHyps {h} ms

def Aesop.ForwardRuleMatches.update (newMatches : Array ForwardRuleMatch) (erasedHyps : Std.HashSet Lean.FVarId) (consumedForwardRuleMatches : Array ForwardRuleMatch) (forwardRuleMatches : ForwardRuleMatches) : ForwardRuleMatches

Update the ForwardRuleMatches of a goal so that they are suitable for a child goal. newMatches are new forward rule matches obtained by updating the old goal's ForwardState with new hypotheses from the new goal. erasedHyps are the hypotheses from the old goal that no longer appear in the new goal. consumedForwardRuleMatches contains forward rule matches that were applied as rules to transform the old goal into the new goal.

Equations

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

def Aesop.ForwardRuleMatches.normRules (ms : ForwardRuleMatches) : Array NormRule

Get the norm rules corresponding to the norm rule matches.

Equations

• ms.normRules = (Aesop.forwardRuleMatchesToNormRules? (Aesop.ForwardRuleMatches.pHashSetToArray✝ ms.normMatches)).get!

def Aesop.ForwardRuleMatches.safeRules (ms : ForwardRuleMatches) : Array SafeRule

Get the safe rules corresponding to the safe rule matches.

Equations

• ms.safeRules = (Aesop.forwardRuleMatchesToSafeRules? (Aesop.ForwardRuleMatches.pHashSetToArray✝ ms.safeMatches)).get!

def Aesop.ForwardRuleMatches.unsafeRules (ms : ForwardRuleMatches) : Array UnsafeRule

Get the unsafe rules corresponding to the unsafe rule matches.

Equations

• ms.unsafeRules = (Aesop.forwardRuleMatchesToUnsafeRules? (Aesop.ForwardRuleMatches.pHashSetToArray✝ ms.unsafeMatches)).get!

def Aesop.ForwardRuleMatches.size (ms : ForwardRuleMatches) : Nat

O(n) Number of matches in ms.

Equations

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