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

feat(frontends/lean/pp): all disables numerals

Browse source
This commit is contained in:
Daniel Selsam 2015-12-10 17:38:48 -08:00 committed by Leonardo de Moura
parent abbb2cfbbd
commit 2b1e7e7759
4 changed files with 23 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -280,7 +280,7 @@ void pretty_fn::set_options_core(options const & o) {
m_purify_metavars = get_pp_purify_metavars(o); m_purify_metavars = get_pp_purify_metavars(o);
m_purify_locals = get_pp_purify_locals(o); m_purify_locals = get_pp_purify_locals(o);
m_beta = !all && get_pp_beta(o); m_beta = !all && get_pp_beta(o);
m_numerals = get_pp_numerals(o); m_numerals = !all && get_pp_numerals(o);
m_abbreviations = !all && get_pp_abbreviations(o); m_abbreviations = !all && get_pp_abbreviations(o);
m_preterm = get_pp_preterm(o); m_preterm = get_pp_preterm(o);
m_hide_full_terms = get_formatter_hide_full_terms(o); m_hide_full_terms = get_formatter_hide_full_terms(o);

7
tests/lean/binder_overload.lean.expected.out
View file

@ -1,7 +1,8 @@
{x : ℕ ∈ S | x > 0} : set ℕ {x : ℕ ∈ S | x > 0} : set ℕ
{x : ℕ ∈ s | x > 0} : finset ℕ {x : ℕ ∈ s | x > 0} : finset ℕ
@set.sep.{1} nat (λ (x : nat), @gt.{1} nat _source.to.has_lt x 0) S : set.{1} nat @set.sep.{1} nat (λ (x : nat), @gt.{1} nat _source.to.has_lt x (@zero.{1} nat _source.to.has_zero)) S : set.{1} nat
@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), @gt.{1} nat _source.to.has_lt x 0) @finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b)
(λ (a : nat), nat.decidable_lt 0 a) (λ (x : nat), @gt.{1} nat _source.to.has_lt x (@zero.{1} nat _source.to.has_zero))
(λ (a : nat), nat.decidable_lt (@zero.{1} nat _source.to.has_zero) a)
s : s :
finset.{1} nat finset.{1} nat

8
tests/lean/pp_all.lean.expected.out
View file

@ -1,2 +1,8 @@
a + of_num b = 10 : Prop a + of_num b = 10 : Prop
@eq.{1} nat (@add.{1} nat _source.to.has_add ((λ (x : nat), x) a) (nat.of_num 2)) 10 : Prop @eq.{1} nat
(@add.{1} nat _source.to.has_add ((λ (x : nat), x) a)
(nat.of_num (@bit0.{1} num num_has_add (@one.{1} num num_has_one))))
(@bit0.{1} nat _source.to.has_add
(@bit1.{1} nat _source.to.has_one _source.to.has_add
(@bit0.{1} nat _source.to.has_add (@one.{1} nat _source.to.has_one)))) :
Prop

12
tests/lean/replace1.lean.expected.out
View file

@ -7,4 +7,14 @@ replace1.lean:29:9: error: #replace commad failed
@eq.rec.{0 1} nat a (λ (x : nat), p x) H1 b (@eq.refl.{1} nat a) @eq.rec.{0 1} nat a (λ (x : nat), p x) H1 b (@eq.refl.{1} nat a)
@eq.rec.{0 1} nat a (λ (x : nat), p x) H1 a (@eq.refl.{1} nat a) @eq.rec.{0 1} nat a (λ (x : nat), p x) H1 a (@eq.refl.{1} nat a)
replace1.lean:40:9: error: #replace commad failed replace1.lean:40:9: error: #replace commad failed
λ (v₁ v₂ : bv 11), @eq.{1} (bv 11) v₁ v₂ λ
(v₁ v₂ :
bv
(@bit1.{1} nat nat_has_one nat_has_add
(@bit1.{1} nat nat_has_one nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one))))),
@eq.{1}
(bv
(@bit1.{1} nat nat_has_one nat_has_add
(@bit1.{1} nat nat_has_one nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one)))))
v₁
v₂