lean2/tests/lean/tst10.lean

variable a : Bool
variable b : Bool
-- Conjunctions
print a && b
print a && b && a
print a /\ b
print a ∧ b
print (and a b)
print and a b
-- Disjunctions
print a || b
print a \/ b
print a ∨ b
print (or a b)
print or a (or a b)
-- Simple Formulas
print a → b → a
check a → b
eval a → a
eval true → a
-- Simple proof
axiom H1 : a
axiom H2 : a → b
-												feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-05 20:05:08 +00:00
+								variable a : Bool
 								variable b : Bool
-												chore(*): cleanup lean builtin symbols, replace :: with _

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-09 16:33:52 +00:00
+								-- Conjunctions
-												feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-05 19:03:35 +00:00
+								print a && b
 								print a && b && a
 								print a /\ b
 								print a ∧ b
 								print (and a b)
 								print and a b
-												feat(frontends/lean/scanner): use Lua style comments in Lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-05 16:52:46 +00:00
+								-- Disjunctions
-												feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-05 19:03:35 +00:00
+								print a || b
 								print a \/ b
 								print a ∨ b
 								print (or a b)
 								print or a (or a b)
-												feat(frontends/lean/scanner): use Lua style comments in Lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-05 16:52:46 +00:00
+								-- Simple Formulas
-												feat(kernel): use Pi as forall/implication

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-08 08:38:39 +00:00
+								print a → b → a
 								check a → b
 								eval a → a
 								eval true → a
-												feat(frontends/lean/scanner): use Lua style comments in Lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-05 16:52:46 +00:00
+								-- Simple proof
-												feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-05 20:05:08 +00:00
+								axiom H1 : a
-												feat(kernel): use Pi as forall/implication

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-08 08:38:39 +00:00
+								axiom H2 : a → b