chore: display LCNF unreachable type when pp.all is true

This commit is contained in:
Leonardo de Moura 2022-10-31 07:23:25 -07:00
parent 4bf2df563d
commit 67e2735f07

View file

@ -99,7 +99,11 @@ mutual
| .cases c => return f!"cases {← ppFVar c.discr} : {← ppExpr c.resultType}{← prefixJoin .line c.alts ppAlt}"
| .return fvarId => return f!"return {← ppFVar fvarId}"
| .jmp fvarId args => return f!"goto {← ppFVar fvarId} {← ppArgs args}"
| .unreach .. => return "⊥"
| .unreach type =>
if pp.all.get (← getOptions) then
return f!"⊥ : {← ppExpr type}"
else
return "⊥"
end
def run (x : M α) : CompilerM α :=