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.

instance Aesop.instInhabitedForwardRuleMatches : Inhabited ForwardRuleMatches

def Aesop.ForwardRuleMatches.empty : ForwardRuleMatches

Empty ForwardRuleMatches.

instance Aesop.ForwardRuleMatches.instEmptyCollection : EmptyCollection ForwardRuleMatches

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

Add a complete match.

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

Add several complete matches.

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

Erase a complete match.

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

Erase several complete matches.

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

Build a ForwardRuleMatches structure containing the matches from ms.

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

Erase matches containing any of the hypotheses hs from ms.

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

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

Erase matches containing the hypothesis h from 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.

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

Get the norm rules corresponding to the norm rule matches.

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

Get the safe rules corresponding to the safe rule matches.

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

Get the unsafe rules corresponding to the unsafe rule matches.

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

O(n) Number of matches in ms.