diff options
Diffstat (limited to 'test-suite/output/Binder.out')
| -rw-r--r-- | test-suite/output/Binder.out | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out index 34558e9a6b..9c46ace463 100644 --- a/test-suite/output/Binder.out +++ b/test-suite/output/Binder.out @@ -1,8 +1,12 @@ -foo = fun '(x, y) => x + y +Monomorphic foo = fun '(x, y) => x + y : nat * nat -> nat + +foo is not universe polymorphic forall '(a, b), a /\ b : Prop -foo = λ '(x, y), x + y +Monomorphic foo = λ '(x, y), x + y : nat * nat → nat + +foo is not universe polymorphic ∀ '(a, b), a ∧ b : Prop |