lean2/examples/lean/ex4.lean

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
Add proof by evaluation examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-06 01:55:22 +00:00			`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 *)`
Fix typo 2013-09-06 02:18:55 +00:00			`Theorem T3 : a > 11 := Trivial`