fix(frontends/lean/builtin_cmds): fixes #671

This commit is contained in:
Leonardo de Moura 2015-06-13 11:32:59 -07:00
parent 9fbf267a3f
commit 591fb91f34
7 changed files with 25 additions and 19 deletions

View file

@ -174,7 +174,7 @@ static void print_definition(parser const & p, name const & n, pos_info const &
io_state_stream new_out = out.update_options(opts);
if (d.is_axiom())
throw parser_error(sstream() << "invalid 'print definition', theorem '" << n
<< "' is not available (suggestion: use command 'wait " << n << "')", pos);
<< "' is not available (suggestion: use command 'reveal " << n << "')", pos);
if (!d.is_definition())
throw parser_error(sstream() << "invalid 'print definition', '" << n << "' is not a definition", pos);
new_out << d.get_value() << endl;
@ -265,13 +265,16 @@ static void print_recursor_info(parser & p) {
}
}
bool print_constant(parser & p, char const * kind, declaration const & d) {
bool print_constant(parser & p, char const * kind, declaration const & d, bool is_def = false) {
io_state_stream out = p.regular_stream();
if (is_protected(p.env(), d.get_name()))
out << "protected ";
out << kind << " " << d.get_name();
print_attributes(p, d.get_name());
out << " : " << d.get_type() << "\n";
out << " : " << d.get_type();
if (is_def)
out << " :=";
out << "\n";
return true;
}
@ -287,7 +290,7 @@ bool print_polymorphic(parser & p) {
for (name const & c : cs) {
declaration const & d = env.get(c);
if (d.is_theorem()) {
print_constant(p, "theorem", d);
print_constant(p, "theorem", d, true);
print_definition(p, c, pos);
} else if (d.is_axiom() || d.is_constant_assumption()) {
if (inductive::is_inductive_decl(env, c)) {
@ -306,7 +309,7 @@ bool print_polymorphic(parser & p) {
print_constant(p, "constant", d);
}
} else if (d.is_definition()) {
print_constant(p, "definition", d);
print_constant(p, "definition", d, true);
print_definition(p, c, pos);
}
}

View file

@ -1,5 +1,5 @@
foo : Π (A : Type) [H : inhabited A], A → A
foo' : Π {A : Type} [H : inhabited A] {x : A}, A
foo 10 :
definition test : ∀ {A : Type} [H : inhabited A], @foo' num num.is_inhabited 10 = 10
definition test : ∀ {A : Type} [H : inhabited A], @foo' num num.is_inhabited 10 = 10 :=
λ (A : Type) (H : inhabited A), @rfl num (@foo' num num.is_inhabited 10)

View file

@ -1,6 +1,6 @@
definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a
definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a :=
ID
definition function.id [reducible] : Π {A : Type}, A → A
definition function.id [reducible] : Π {A : Type}, A → A :=
λ (A : Type) (a : A), a
-----------
definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a

1
tests/lean/671.lean Normal file
View file

@ -0,0 +1 @@
print nat.add

View file

@ -0,0 +1,2 @@
definition nat.add : nat → nat → nat :=
λ (a b : nat), nat.rec_on b a (λ (b₁ : nat), nat.succ)

View file

@ -1,8 +1,8 @@
definition test.foo.prf [irreducible] : ∀ (x : ), 0 < succ (succ x)
definition test.foo.prf [irreducible] : ∀ (x : ), 0 < succ (succ x) :=
λ (x : ), lt.step (zero_lt_succ x)
definition test.bla :
definition test.bla : :=
λ (a : ), foo (succ (succ a)) (foo.prf a)
definition test.bla :
definition test.bla : :=
λ (a : ), test.foo (succ (succ a)) (test.foo.prf a)
definition test.foo.prf : ∀ (x : ), 0 < succ (succ x)
definition test.foo.prf : ∀ (x : ), 0 < succ (succ x) :=
λ (x : ), lt.step (zero_lt_succ x)

View file

@ -1,15 +1,15 @@
definition bla :
definition bla : :=
λ (a : ), foo (succ (succ a)) (bla_2 a)
definition bla_1 : ∀ (x : ), 0 < succ x
definition bla_1 : ∀ (x : ), 0 < succ x :=
λ (x : ), zero_lt_succ x
definition bla_2 : ∀ (x : ), 0 < succ (succ x)
definition bla_2 : ∀ (x : ), 0 < succ (succ x) :=
λ (x : ), lt.step (bla_1 x)
definition test_1 [irreducible] : ∀ (x : ), 0 < succ x
definition test_1 [irreducible] : ∀ (x : ), 0 < succ x :=
λ (x : ), zero_lt_succ x
definition test_2 [reducible] : ∀ (x : ), 0 < succ (succ x)
definition test_2 [reducible] : ∀ (x : ), 0 < succ (succ x) :=
λ (x : ), lt.step (test_1 x)
definition tst_1 : ∀ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x),
x_1 :: x_2 = nil.{l_1} → list.no_confusion_type.{0 l_1} false (x_1 :: x_2) nil.{l_1}
x_1 :: x_2 = nil.{l_1} → list.no_confusion_type.{0 l_1} false (x_1 :: x_2) nil.{l_1} :=
λ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x), list.no_confusion.{0 l_1}
definition tst : Π {A : Type.{l_1}}, A → list.{l_1} A → bool
definition tst : Π {A : Type.{l_1}}, A → list.{l_1} A → bool :=
λ (A : Type.{l_1}) (a : A) (l : list.{l_1} A), voo.{(max 1 l_1)} (a :: l) nil.{l_1} (tst_1.{l_1} A a l)