structure Aesop.FVarIdSubst : Type

• map : Std.HashMap Lean.FVarId Lean.FVarId

Instances For

• Aesop.FVarIdSubst.instEmptyCollection
• Aesop.instInhabitedFVarIdSubst

instance Aesop.instInhabitedFVarIdSubst : Inhabited Aesop.FVarIdSubst

Equations

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

def Aesop.FVarIdSubst.isEmpty (s : Aesop.FVarIdSubst) : Bool

Equations

• s.isEmpty = s.map.isEmpty

def Aesop.FVarIdSubst.contains (s : Aesop.FVarIdSubst) (fvarId : Lean.FVarId) : Bool

Equations

• s.contains fvarId = s.map.contains fvarId

def Aesop.FVarIdSubst.find? (s : Aesop.FVarIdSubst) (fvarId : Lean.FVarId) : Option Lean.FVarId

Equations

• s.find? fvarId = s.map[fvarId]?

def Aesop.FVarIdSubst.get (s : Aesop.FVarIdSubst) (fvarId : Lean.FVarId) : Lean.FVarId

Equations

• s.get fvarId = (s.find? fvarId).getD fvarId

def Aesop.FVarIdSubst.apply (s : Aesop.FVarIdSubst) (e : Lean.Expr) : Lean.Expr

Equations

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

def Aesop.FVarIdSubst.applyToLocalDecl (s : Aesop.FVarIdSubst) : Lean.LocalDecl → Lean.LocalDecl

Equations

• s.applyToLocalDecl (Lean.LocalDecl.cdecl i id n t bi k) = Lean.LocalDecl.cdecl i id n (s.apply t) bi k
• s.applyToLocalDecl (Lean.LocalDecl.ldecl i id n t v nd k) = Lean.LocalDecl.ldecl i id n (s.apply t) (s.apply v) nd k

def Aesop.FVarIdSubst.domain (s : Aesop.FVarIdSubst) : Std.HashSet Lean.FVarId

Equations

• s.domain = Std.HashMap.fold (fun (r : Std.HashSet Lean.FVarId) (k x : Lean.FVarId) => r.insert k) ∅ s.map

def Aesop.FVarIdSubst.codomain (s : Aesop.FVarIdSubst) : Std.HashSet Lean.FVarId

Equations

• s.codomain = Std.HashMap.fold (fun (r : Std.HashSet Lean.FVarId) (x v : Lean.FVarId) => r.insert v) ∅ s.map

def Aesop.FVarIdSubst.empty : Aesop.FVarIdSubst

Equations

• Aesop.FVarIdSubst.empty = { map := ∅ }

instance Aesop.FVarIdSubst.instEmptyCollection : EmptyCollection Aesop.FVarIdSubst

Equations

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

def Aesop.FVarIdSubst.insert (s : Aesop.FVarIdSubst) (old : Lean.FVarId) (new : Lean.FVarId) : Aesop.FVarIdSubst

Equations

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

def Aesop.FVarIdSubst.erase (s : Aesop.FVarIdSubst) (fvarId : Lean.FVarId) : Aesop.FVarIdSubst

Equations

• s.erase fvarId = { map := s.map.erase fvarId }

def Aesop.FVarIdSubst.append (s : Aesop.FVarIdSubst) (t : Aesop.FVarIdSubst) : Aesop.FVarIdSubst

Equations

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

def Aesop.FVarIdSubst.ofFVarSubstIgnoringNonFVarIds (s : Lean.Meta.FVarSubst) : Aesop.FVarIdSubst

Equations

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

def Aesop.FVarIdSubst.ofFVarSubst? (s : Lean.Meta.FVarSubst) : Option Aesop.FVarIdSubst

Equations

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