aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4203.v
blob: 076a3c3d68239130b22e21ab431e8c4431a0fec6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Set Primitive Projections.

Record ops {T:Type} := { is_ok : T -> Prop; constant : T }.
Arguments ops : clear implicits.

Record ops_ok {T} (Ops:ops T) := { constant_ok : is_ok Ops (constant Ops) }.

Definition nat_ops : ops nat := {| is_ok := fun n => n = 1; constant := 1 |}.
Definition nat_ops_ok : ops_ok nat_ops.
Proof.
  split. cbn. apply eq_refl.
Qed.

Definition t := Eval lazy in constant_ok nat_ops nat_ops_ok.
Definition t' := Eval vm_compute in constant_ok nat_ops nat_ops_ok.
Definition t'' := Eval native_compute in constant_ok nat_ops nat_ops_ok.

Check (eq_refl t : t = t').
Check (eq_refl t : t = t'').