From 71d76a891ce4ef5120d44ea0439478232f8eb314 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Sep 2013 18:55:22 -0700 Subject: [PATCH] Add proof by evaluation examples Signed-off-by: Leonardo de Moura --- examples/lean/ex4.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 examples/lean/ex4.lean diff --git a/examples/lean/ex4.lean b/examples/lean/ex4.lean new file mode 100644 index 000000000..827d98c8d --- /dev/null +++ b/examples/lean/ex4.lean @@ -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 \ No newline at end of file