aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/univscompute.v
blob: 1d60ab360c08e7d767fd21355b505f5651d8d248 (plain)
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
Set Universe Polymorphism.

Polymorphic Definition id {A : Type} (a : A) := a.

Eval vm_compute in id 1.

Polymorphic Inductive ind (A : Type) := cons : A -> ind A.

Eval vm_compute in ind unit.

Check ind unit.

Eval vm_compute in ind unit.

Definition bar := Eval vm_compute in ind unit.
Definition bar' := Eval vm_compute in id (cons _ tt).

Definition bar'' := Eval native_compute in id 1.
Definition bar''' := Eval native_compute in id (cons _ tt).

Definition barty := Eval native_compute in id (cons _ Set).

Definition one := @id.

Monomorphic Definition sec := one.

Eval native_compute in sec.
Definition sec' := Eval native_compute in sec.
Eval vm_compute in sec.
Definition sec'' := Eval vm_compute in sec.