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

chore(frontends/lean,tests): fix tests and style

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-09 10:29:34 -07:00
parent 53236718a8
commit a5fb28ca78
4 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1542,7 +1542,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
new_as.push_back(*r); new_as.push_back(*r);
bool has_constructor = false; bool has_constructor = false;
for (auto const & e : as) { for (auto const & e : as) {
has_constructor |= (bool)inductive::is_intro_rule(m_env, e); has_constructor |= static_cast<bool>(inductive::is_intro_rule(m_env, e));
new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p)); new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p));
} }
if (m_undef_id_behavior == undef_id_behavior::AssumeLocalAndAlsoDefinedNonConstructors && if (m_undef_id_behavior == undef_id_behavior::AssumeLocalAndAlsoDefinedNonConstructors &&

2
tests/lean/630.lean.expected.out
View file

@ -1,4 +1,4 @@
definition pnat.pnat : Type₁ := definition pnat : Type₁ :=
{n | n > 0} {n | n > 0}
inductive prod : Type → Type → Type inductive prod : Type → Type → Type
constructors: constructors:

4
tests/lean/run/eq2.lean
View file

@ -1,5 +1,5 @@
definition symm {A : Type} : Π {a b : A}, a = b → b = a definition symm {A : Type} : Π {a b : A}, a = b → b = a
| a a rfl := rfl | a a (eq.refl a) := rfl
definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
| a a a rfl rfl := rfl | a a a (eq.refl a) (eq.refl a) := rfl

2
tests/lean/run/match_tac.lean
View file

@ -16,4 +16,4 @@ end
open nat open nat
example : ∀ (a b : nat), a = b → b = a example : ∀ (a b : nat), a = b → b = a
| a a rfl := rfl | a a (eq.refl a) := rfl