fix(frontends/lean/util): fixes #1495

We should freeze only constants
This commit is contained in:
Leonardo de Moura 2017-03-28 11:55:11 -07:00
parent 07c29c0779
commit 092985f777
2 changed files with 11 additions and 1 deletions

View file

@ -418,7 +418,7 @@ bool is_frozen_name(expr const & e) {
expr freeze_names(expr const & e) {
return replace(e, [&](expr const e, unsigned) {
if (is_local(e) || is_constant(e))
if (is_constant(e))
return some_expr(mk_frozen_name_annotation(e));
else
return none_expr();

10
tests/lean/run/1495.lean Normal file
View file

@ -0,0 +1,10 @@
section
variables (r : → Prop)
local infix `≼` : 50 := r
example {a b : } : a ≼ b → true :=
begin
show a ≼ b → true,
from λx, trivial
end
end