Add small example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-18 10:59:59 -07:00
parent 843253355b
commit 85222e13ba

26
examples/ex1.lean Normal file
View file

@ -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