michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/pp): display implicit arguments when expression contains metavariables

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-13 12:42:05 -08:00
parent d83a13d044
commit 12451e4a35
3 changed files with 19 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/pp.cpp
View file

@ -640,7 +640,7 @@ class pp_fn {
result pp_app(expr const & e, unsigned depth) {
if (!m_coercion && is_coercion(e))
return pp(arg(e, 1), depth);
application app(e, *this, m_implict);
application app(e, *this, m_implict || has_metavar(e));
operator_info op;
if (m_notation && app.notation_enabled() && (op = get_operator(e)) && has_expected_num_args(app, op)) {
result p_arg;

4
tests/lean/elab1.lean.expected.out
View file

@ -44,8 +44,8 @@ Failed to solve
a
a
b
refl a
refl b
@refl ?M::5 a
@refl ?M::6 b
Failed to solve
⊢ ?M::1 ≺ Type
elab1.lean:22:6: Type of argument 1 must be convertible to the expected type in the application of

17
tests/lean/induction2.lean.expected.out
View file

@ -11,4 +11,19 @@ Failed to solve
?M::3
λ m : ℕ, Nat::add_zerol m ⋈ symm (Nat::add_zeror m)
λ (n : ℕ) (iH : ?M::3 n) (m : ℕ),
Nat::add_succl n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add_succr m n)
@trans ℕ
(n + 1 + m)
(m + n + 1)
(m + (n + 1))
(@trans ℕ
(n + 1 + m)
(n + m + 1)
(m + n + 1)
(Nat::add_succl n m)
(@subst ?M::14
?M::15
?M::16
(λ x : ?M::14, (?M::48[lift:0:1]) x == (?M::49[lift:0:1]) x)
(refl (n + m + 1))
iH))
(symm (Nat::add_succr m n))