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

feat(frontends/lean/builtin_cmds): show metavariable arguments when pretty printing patterns

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-07 12:39:51 -08:00
parent 0f76e33724
commit c3b5ce0785
3 changed files with 20 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/builtin_cmds.cpp
View file

@ -240,7 +240,10 @@ static void print_patterns(parser & p, name const & n) {
blast::scope_debug scope(p.env(), p.ios());
auto hi = blast::mk_hi_lemma(n, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY);
if (hi.m_multi_patterns) {
io_state_stream out = p.regular_stream();
io_state_stream _out = p.regular_stream();
options opts = _out.get_options();
opts = opts.update_if_undef(get_pp_metavar_args_name(), true);
io_state_stream out = _out.update_options(opts);
out << "(multi-)patterns:\n";
if (!is_nil(hi.m_mvars)) {
expr m = head(hi.m_mvars);

11
tests/lean/pattern_pp.lean Normal file
View file

@ -0,0 +1,11 @@
definition Sum : nat → (nat → nat) → nat := sorry
definition Sum_weird [forward] (f g h : nat → nat) (n : nat) : (Sum n (λ x, f (g (h x)))) = 1 := sorry
print Sum_weird
/-
definition Sum_weird [forward] : ∀ (f g h : nat → nat) (n : nat), eq (Sum n (λ (x : nat), f (g (h x)))) 1 :=
λ (f g h : nat → nat) (n : nat), sorry
(multi-)patterns:
?M_1 : nat → nat, ?M_2 : nat → nat, ?M_3 : nat → nat, ?M_4 : nat
{Sum ?M_4 (λ (x : nat), ?M_1)}
-/

5
tests/lean/pattern_pp.lean.expected.out Normal file
View file

@ -0,0 +1,5 @@
definition Sum_weird [forward] : ∀ (f g h : ℕ → ℕ) (n : ℕ), Sum n (λ (x : ℕ), f (g (h x))) = 1 :=
λ (f g h : ℕ → ℕ) (n : ℕ), sorry
(multi-)patterns:
?M_1 : ℕ → ℕ, ?M_2 : ℕ → ℕ, ?M_3 : ℕ → ℕ, ?M_4 : ℕ
{Sum ?M_4 (λ (x : ℕ), ?M_1 (?M_2 (?M_3 x)))}