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

Add proof by evaluation examples

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-05 18:55:22 -07:00
parent c22bd8b6ed
commit 71d76a891c
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
examples/lean/ex4.lean Normal file
View file

@ -0,0 +1,6 @@
Definition a : Nat := 10
(* Trivial indicates a "proof by evaluation" *)
Theorem T1 : a > 0 := Trivial
Theorem T2 : a - 5 > 3 := Trivial
(* The next one fails *)
Theorem T3- : a > 11 := Trivial