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

Equations

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

def Aesop.ForwardRuleMatches.empty : ForwardRuleMatches

Empty ForwardRuleMatches.

Equations

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

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.eraseHyps.go (hs : Std.HashSet Lean.FVarId) (ms : Lean.PHashSet ForwardRuleMatch) : Lean.PHashSet ForwardRuleMatch

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) (consumedForwardRuleMatch? : Option 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. consumedForwardRuleMatch? is a forward rule match that was applied as a rule 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.foldNormRules {σ : Type u_1} (ms : ForwardRuleMatches) (f : σ → NormRule → σ) (init : σ) : σ

Fold over the norm rules corresponding to the norm rule matches.

Equations

• ms.foldNormRules f init = Aesop.ForwardRuleMatches.foldRules!✝ ms.normMatches (fun (x : Aesop.ForwardRuleMatch) => x.toNormRule?) f init

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

Get the norm rules corresponding to the norm rule matches.

Equations

• ms.normRules = ms.foldNormRules (fun (x1 : Array Aesop.NormRule) (x2 : Aesop.NormRule) => x1.push x2) #[]

def Aesop.ForwardRuleMatches.foldSafeRules {σ : Type u_1} (ms : ForwardRuleMatches) (f : σ → SafeRule → σ) (init : σ) : σ

Fold over the safe rules corresponding to the safe rule matches.

Equations

• ms.foldSafeRules f init = Aesop.ForwardRuleMatches.foldRules!✝ ms.safeMatches (fun (x : Aesop.ForwardRuleMatch) => x.toSafeRule?) f init

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

Get the safe rules corresponding to the safe rule matches.

Equations

• ms.safeRules = ms.foldSafeRules (fun (x1 : Array Aesop.SafeRule) (x2 : Aesop.SafeRule) => x1.push x2) #[]

def Aesop.ForwardRuleMatches.foldUnsafeRules {σ : Type u_1} (ms : ForwardRuleMatches) (f : σ → UnsafeRule → σ) (init : σ) : σ

Fold over the unsafe rules corresponding to the unsafe rule matches.

Equations

• ms.foldUnsafeRules f init = Aesop.ForwardRuleMatches.foldRules!✝ ms.unsafeMatches (fun (x : Aesop.ForwardRuleMatch) => x.toUnsafeRule?) f init

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

Get the unsafe rules corresponding to the unsafe rule matches.

Equations

• ms.unsafeRules = ms.foldUnsafeRules (fun (x1 : Array Aesop.UnsafeRule) (x2 : Aesop.UnsafeRule) => x1.push x2) #[]

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.