structure Aesop.FVarIdSubst : Type

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

@[implicit_reducible]

instance Aesop.instInhabitedFVarIdSubst : Inhabited FVarIdSubst

Equations

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

def Aesop.instInhabitedFVarIdSubst.default : FVarIdSubst

Equations

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

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

Equations

• s.isEmpty = s.map.isEmpty

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.FVarIdSubst.applyToLocalDecl (s : 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 : 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 : 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 : FVarIdSubst

Equations

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

@[implicit_reducible]

instance Aesop.FVarIdSubst.instEmptyCollection : EmptyCollection FVarIdSubst

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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