summaryrefslogtreecommitdiff
path: root/test-suite/output/Binder.out
blob: 34558e9a6b77ebd6ce8de545617a4bc4b1acd49f (plain)
1
2
3
4
5
6
7
8
foo = fun '(x, y) => x + y
     : nat * nat -> nat
forall '(a, b), a /\ b
     : Prop
foo = λ '(x, y), x + y
     : nat * nat → nat
∀ '(a, b), a ∧ b
     : Prop