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

test(tests/lean/run): add new test

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-30 21:38:33 -07:00
parent 1e18a76bdb
commit 4f7f66de3f
1 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
tests/lean/run/constr_tac4.lean Normal file
View file

@ -0,0 +1,20 @@
import data.nat
open nat
definition lt.trans {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
have aux : a < b → a < c, from
lt.rec_on H₂
(λ h₁, lt.step h₁)
(λ b₁ bb₁ ih h₁, by constructor; exact ih h₁),
aux H₁
definition succ_lt_succ {a b : nat} (H : a < b) : succ a < succ b :=
lt.rec_on H
(by constructor)
(λ b hlt ih, lt.trans ih (by constructor))
definition lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
lt.rec_on H
(by constructor; constructor)
(λ b h ih, by constructor; exact ih)