]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/tests/match01.cic
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
ignores .toc
[helm.git] / helm / gTopLevel / tests / match01.cic
1 [\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
2 match (le_n O): le with
3 [ le_n \Rightarrow (refl_equal nat O)
4 | (le_S x y) \Rightarrow (refl_equal nat O) ]
Unnamed repository; edit this file 'description' to name the repository.