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

fix: fixes #616

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-07 07:29:54 -07:00
parent 8a84532760
commit a863f1b8a3
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/csimp.cpp
View file

@ -1938,6 +1938,10 @@ class csimp_fn {
case expr_kind::Proj: return visit_proj(e, is_let_val);
case expr_kind::App: return visit_app(e, is_let_val);
case expr_kind::Const: return visit_constant(e, is_let_val);
/* We erase MData for now. We should revisit this decision when we rewrite the compiler in Lean, since we
are probably going to store debugging information in this kind of node.
We erase it here because `ir.cpp` does not support it, and produced `unreachable` code at issue #616 */
case expr_kind::MData: return visit(mdata_expr(e), is_let_val);
default: return e;
}
}

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

@ -0,0 +1,3 @@
def bug : Monad (λ α : Type _ => α → Prop) where
pure x := (.=x)
bind s f y := ∃ x, s x ∧ f x y