1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
From Corelib Require Import PrimInt63 PrimArray.
Class pointed T := point : T.
Inductive PROOF_OF A := the (x : A).
Definition foo : PROOF_OF (@make (pointed nat) 0 0 = @make nat 0 0).
constructor.
cbv. (* @eq (array@{pointed.u0} nat) [| | O : nat |]@{pointed.u0} [| | O : nat |]@{Set} *)
reflexivity.
Defined.
Notation barv
:= (@exist (array@{Set} nat) (fun x => x = @make nat 0 0) _ (eq_refl (@make nat 0 0)))
(only parsing).
Definition bar1 : { x | x = @make (pointed nat) 0 0 }
:= Eval cbv in barv.
Definition bar0 : { x | x = @make (pointed nat) 0 0 }
:= Eval vm_compute in barv.
Definition bar := Eval cbv in foo.
|
