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

fix: bug at compatibleTypes

Browse source 
Many thanks to @hargoniX
This commit is contained in:
Leonardo de Moura 2022-09-13 15:57:12 -07:00
parent 8f2ab82408
commit e8246e026d
2 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Compiler/LCNF/Types.lean
View file

@ -201,9 +201,11 @@ partial def compatibleTypes (a b : Expr) : Bool :=
if a.isAnyType || b.isAnyType then
true
else
let a := a.headBeta
let b := b.headBeta
if a == b then
let a' := a.headBeta
let b' := b.headBeta
if a != a' || b != b' then
compatibleTypes a' b'
else if a == b then
true
else
match a, b with

3
tests/lean/run/compatibleTypesBugAtLCNF.lean Normal file
View file

@ -0,0 +1,3 @@
import Lean
#eval Lean.Compiler.compile #[``Lean.Compiler.LCNF.Simp.etaPolyApp?]