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
|
Module Mono.
Module Transparent.
Fixpoint F (n : nat) (A : Type) {struct n} : nat
with G (n : nat) (A:Type@{_}) {struct n} : nat.
Proof.
1: pose (match n with S n => G n A | 0 => 0 end).
all: exact 0.
Defined.
End Transparent.
Module Opaque.
Fixpoint F (n : nat) (A : Type) {struct n} : nat
with G (n : nat) (A:Type@{_}) {struct n} : nat.
Proof.
1: pose (match n with S n => G n A | 0 => 0 end).
all: exact 0.
Qed.
End Opaque.
End Mono.
Module Poly.
Set Universe Polymorphism.
Module Transparent.
Fixpoint F (n : nat) (A : Type) {struct n} : nat
with G (n : nat) (A:Type@{_}) {struct n} : nat.
Proof.
1: pose (match n with S n => G n A | 0 => 0 end).
all: exact 0.
Defined.
Check F@{_}. Check G@{_}.
End Transparent.
Module Opaque.
Fixpoint F (n : nat) (A : Type) {struct n} : nat
with G (n : nat) (A:Type@{_}) {struct n} : nat.
Proof.
1: pose (match n with S n => G n A | 0 => 0 end).
all: exact 0.
Qed.
Check F@{_}. Check G@{_}.
End Opaque.
End Poly.
|
