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

fix: normFVarImp bug

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-19 21:39:52 -07:00
parent d132efd440
commit 4c19fdbb97
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Compiler/LCNF/CompilerM.lean
View file

@ -124,9 +124,9 @@ where
else
e
private def normFVarImp (s : FVarSubst) (fvarId : FVarId) : FVarId :=
private partial def normFVarImp (s : FVarSubst) (fvarId : FVarId) : FVarId :=
match s.find? fvarId with
| some (.fvar fvarId') => fvarId'
| some (.fvar fvarId') => normFVarImp s fvarId'
| some _ => panic! "invalid LCNF substitution of free variable with expression"
| none => fvarId