Add example with nested quantifiers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
f9cbdb5456
commit
53e4100e1f
1 changed files with 5 additions and 0 deletions
5
examples/ex9.lean
Normal file
5
examples/ex9.lean
Normal file
|
@ -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)
|
Loading…
Reference in a new issue