blob: 9c46ace4630104e3ff2c08a94d41a659316fb62b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Monomorphic foo = fun '(x, y) => x + y
: nat * nat -> nat
foo is not universe polymorphic
forall '(a, b), a /\ b
: Prop
Monomorphic foo = λ '(x, y), x + y
: nat * nat → nat
foo is not universe polymorphic
∀ '(a, b), a ∧ b
: Prop
|