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

test(tests/lean/run): define list append using recursive equations

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-04 17:50:41 -08:00
parent 7fca862fc3
commit 7488378445
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
tests/lean/run/eq6.lean Normal file
View file

@ -0,0 +1,15 @@
import data.list
open list
definition append {A : Type} : list A → list A → list A,
append nil l := l,
append (h :: t) l := h :: (append t l)
theorem append_nil {A : Type} (l : list A) : append nil l = l :=
rfl
theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) :=
rfl
example : append (1 :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
rfl