doc(demo): add another example into demo set

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-28 10:11:58 -08:00
parent 9bdf076342
commit b55aee1efd

25
doc/demo/congr.lean Normal file
View file

@ -0,0 +1,25 @@
rewrite_set simple
add_rewrite and_truer and_truel and_falser and_falsel or_falsel : simple
(*
add_congr_theorem("simple", "and_congr")
add_congr_theorem("simple", "or_congr")
*)
variables a b c : Nat
(*
local t = parse_lean([[a = 1 ∧ (¬ b = 0 c ≠ 0 b + c > a)]])
local s, pr = simplify(t, "simple")
print(s)
print(pr)
print(get_environment():type_check(pr))
*)
exit
check @and_congr
check @or_congr
check @and_congrr
check @and_congrl
import if_then_else
check @if_congr