max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add FVarSubst.domain

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-03 11:35:58 -07:00
parent 252ef7345f
commit ad53983e35
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Meta/Tactic/FVarSubst.lean
View file

@ -63,6 +63,9 @@ else oldS.map.fold
| some fvarId'' => m.insert fvarId fvarId'')
newS
def domain (s : FVarSubst) : List FVarId :=
s.map.fold (fun r k v => k :: r) []
end FVarSubst
end Meta