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

fix(tests/lean/slow): adjust tests

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-01 19:47:55 -07:00
parent 9dc0388022
commit 230b994e79
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/slow/nat_bug2.lean
View file

@ -4,7 +4,7 @@
-- Author: Floris van Doorn -- Author: Floris van Doorn
---------------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------------------------------
import logic algebra.binary import logic algebra.binary
open tactic binary eq.ops eq open binary eq.ops eq
open decidable open decidable
namespace experiment namespace experiment
definition refl := @eq.refl definition refl := @eq.refl
@ -27,7 +27,7 @@ definition to_nat [coercion] (n : num) : ℕ
:= num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n := num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
namespace helper_tactics namespace helper_tactics
definition apply_refl := apply @refl definition apply_refl := tactic.apply @refl
tactic_hint apply_refl tactic_hint apply_refl
end helper_tactics end helper_tactics
open helper_tactics open helper_tactics

4
tests/lean/slow/nat_wo_hints.lean
View file

@ -4,7 +4,7 @@
-- Author: Floris van Doorn -- Author: Floris van Doorn
---------------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------------------------------
import logic algebra.binary import logic algebra.binary
open tactic binary eq.ops eq open binary eq.ops eq
open decidable open decidable
namespace experiment namespace experiment
@ -23,7 +23,7 @@ definition to_nat [coercion] (n : num) : ℕ
:= num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n := num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
namespace helper_tactics namespace helper_tactics
definition apply_refl := apply @eq.refl definition apply_refl := tactic.apply @eq.refl
tactic_hint apply_refl tactic_hint apply_refl
end helper_tactics end helper_tactics
open helper_tactics open helper_tactics