From 85222e13ba3087c831d6e260cd8bb3a685f0c21e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Aug 2013 10:59:59 -0700 Subject: [PATCH] Add small example Signed-off-by: Leonardo de Moura --- examples/ex1.lean | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 examples/ex1.lean diff --git a/examples/ex1.lean b/examples/ex1.lean new file mode 100644 index 0000000000..a2ee83e011 --- /dev/null +++ b/examples/ex1.lean @@ -0,0 +1,26 @@ +Variable a : Bool +Variable b : Bool +(* Conjunctions *) +Show a && b +Show a && b && a +Show a /\ b +Show a ∧ b +Show (and a b) +Show and a b +(* Disjunctions *) +Show a || b +Show a \/ b +Show a ∨ b +Show (or a b) +Show or a (or a b) +(* Simple Formulas *) +Show a => b => a +Check a => b +Eval a => a +Eval true => a +(* Simple proof *) +Axiom H1 : a +Axiom H2 : a => b +Check MP +Show MP a b H2 H1 +Check MP a b H2 H1