From 09af93186a532a9bd606fd14f3ec37512fddcb39 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 21 Jun 2017 03:44:12 -0400 Subject: [PATCH] fix(frontends/lean/elaborator): @applications don't make thunks --- library/data/lazy_list.lean | 2 +- src/frontends/lean/elaborator.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/data/lazy_list.lean b/library/data/lazy_list.lean index 2f98efca32..ac47b4fc1d 100644 --- a/library/data/lazy_list.lean +++ b/library/data/lazy_list.lean @@ -29,7 +29,7 @@ def tail : lazy_list α → lazy_list α def append : lazy_list α → thunk (lazy_list α) → lazy_list α | nil l := l () -| (cons h t) l := cons h (append (t ()) (l ())) +| (cons h t) l := cons h (@append (t ()) l) def map (f : α → β) : lazy_list α → lazy_list β | nil := nil diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 95aeee2e8a..f568bb22d2 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1516,7 +1516,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer< } else if (i < args.size()) { expr expected_type = d; optional thunk_of; - if (!m_in_pattern) thunk_of = is_thunk(d); + if (!m_in_pattern && amask == arg_mask::Default) thunk_of = is_thunk(d); if (thunk_of) expected_type = *thunk_of; // explicit argument expr ref_arg = get_ref_for_child(args[i], ref);