Some tactics substitute hypotheses with expressions.
We track these substitutions using FVarSubst
.
It is just a mapping from the original FVarId (internal) name
to an expression. The free variables occurring in the expression must
be defined in the new goal.
Instances For
Equations
Equations
Instances For
Equations
- s.contains fvarId = Lean.AssocList.contains fvarId s.map
Instances For
Add entry fvarId |-> v
to s
if s
does not contain an entry for fvarId
.
Equations
Instances For
Equations
- s.find? fvarId = Lean.AssocList.find? fvarId s.map
Instances For
Equations
- s.get fvarId = match Lean.AssocList.find? fvarId s.map with | none => Lean.mkFVar fvarId | some v => v
Instances For
Given e
, for each (x => v)
in s
replace x
with v
in e
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- s.domain = Lean.AssocList.foldl (fun (r : List Lean.FVarId) (k : Lean.FVarId) (x : Lean.Expr) => k :: r) [] s.map
Instances For
Equations
Instances For
Constructs a substitution consisting of s
followed by t
.
This satisfies (s.append t).apply e = t.apply (s.apply e)
Equations
- s.append t = Lean.AssocList.foldl (fun (s' : Lean.Meta.FVarSubst) (k : Lean.FVarId) (v : Lean.Expr) => s'.insert k (t.apply v)) t s.map
Instances For
Equations
- Lean.LocalDecl.applyFVarSubst s (Lean.LocalDecl.cdecl i id n t bi k) = Lean.LocalDecl.cdecl i id n (s.apply t) bi k
- Lean.LocalDecl.applyFVarSubst s (Lean.LocalDecl.ldecl i id n t v nd k) = Lean.LocalDecl.ldecl i id n (s.apply t) (s.apply v) nd k