From 53e4100e1f35ed0e41c06980d2c5441b9705d3d3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Aug 2013 15:58:23 -0700 Subject: [PATCH] Add example with nested quantifiers Signed-off-by: Leonardo de Moura --- examples/ex9.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 examples/ex9.lean diff --git a/examples/ex9.lean b/examples/ex9.lean new file mode 100644 index 000000000..c335b8f2e --- /dev/null +++ b/examples/ex9.lean @@ -0,0 +1,5 @@ +Variable f : Type -> Bool +Variable g : Type -> Type -> Bool +Show forall (a b : Type), exists (c : Type), (g a b) = (f c) +Check forall (a b : Type), exists (c : Type), (g a b) = (f c) +Eval forall (a b : Type), exists (c : Type), (g a b) = (f c)