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

chore: workaround for compiler closed term extraction issue

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-01 08:35:00 -08:00
parent 5948003601
commit 85a1a5233b
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Compiler/IR/SimpCase.lean
View file

@ -43,8 +43,11 @@ private def addDefault (alts : Array Alt) : Array Alt :=
let alts := alts.filter fun alt => alt.body != max.body
alts.push (Alt.default max.body)
private def filterUnreachable (alts : Array Alt) : Array Alt :=
alts.filter fun alt => alt.body != FnBody.unreachable
private def mkSimpCase (tid : Name) (x : VarId) (xType : IRType) (alts : Array Alt) : FnBody :=
let alts := alts.filter (fun alt => alt.body != FnBody.unreachable);
let alts := filterUnreachable alts
let alts := addDefault alts;
if alts.size == 0 then
FnBody.unreachable