From dc203b28db8b2e398b82207df087a40fbc9fbe82 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Nov 2015 19:27:44 -0800 Subject: [PATCH] test(tests/lean/run): add more tests --- tests/lean/run/app_builder4.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/lean/run/app_builder4.lean diff --git a/tests/lean/run/app_builder4.lean b/tests/lean/run/app_builder4.lean new file mode 100644 index 0000000000..464f9305fe --- /dev/null +++ b/tests/lean/run/app_builder4.lean @@ -0,0 +1,16 @@ +import data.list + +constants f : nat → nat → nat +constants a b : nat +axiom H2 : a = b +set_option pp.all true + +#app_builder congr (eq.refl (f a)), H2 + +constants g : ∀ {A :Type}, A → A → A +variables A : Type +variables l₁ l₂ l₃: list A +variables H : l₂ = l₃ + +#app_builder congr (eq.refl (g l₁)), H +#app_builder congr_arg (g l₁), H