1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
Monomorphic swap = fun '(x, y) => (y, x)
: A * B -> B * A
swap is not universe polymorphic
fun '(x, y) => (y, x)
: A * B -> B * A
forall '(x, y), swap (x, y) = (y, x)
: Prop
Monomorphic proj_informative =
fun '(exist _ x _) => x : A
: {x : A | P x} -> A
proj_informative is not universe polymorphic
Monomorphic foo =
fun '(Bar n b tt p) => if b then n + p else n - p
: Foo -> nat
foo is not universe polymorphic
Monomorphic baz =
fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
: Foo -> Foo -> nat
baz is not universe polymorphic
Monomorphic swap =
fun (A B : Type) '(x, y) => (y, x)
: forall A B : Type, A * B -> B * A
swap is not universe polymorphic
Arguments A, B are implicit and maximally inserted
Argument scopes are [type_scope type_scope _]
fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
: forall A B : Type, A * B -> Prop
forall (A B : Type) '(x, y), swap (x, y) = (y, x)
: Prop
exists '(x, y), swap (x, y) = (y, x)
: Prop
exists '(x, y) '(z, w), swap (x, y) = (z, w)
: Prop
λ '(x, y), (y, x)
: A * B → B * A
∀ '(x, y), swap (x, y) = (y, x)
: Prop
Monomorphic both_z =
fun pat : nat * nat =>
let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
: forall pat : nat * nat, F pat
both_z is not universe polymorphic
fun '(x, y) '(z, t) => swap (x, y) = (z, t)
: A * B -> B * A -> Prop
forall '(x, y) '(z, t), swap (x, y) = (z, t)
: Prop
fun (pat : nat) '(x, y) => x + y = pat
: nat -> nat * nat -> Prop
Monomorphic f = fun x : nat => x + x
: nat -> nat
f is not universe polymorphic
Argument scope is [nat_scope]
fun x : nat => x + x
: nat -> nat
|
