From b55aee1efd1c7ca193ae7538c05b59b5b5ad46f5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Jan 2014 10:11:58 -0800 Subject: [PATCH] doc(demo): add another example into demo set Signed-off-by: Leonardo de Moura --- doc/demo/congr.lean | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 doc/demo/congr.lean diff --git a/doc/demo/congr.lean b/doc/demo/congr.lean new file mode 100644 index 000000000..a0d5d980f --- /dev/null +++ b/doc/demo/congr.lean @@ -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