blob: a3a39470ed0c029c5181d51c5df762af24af4d39 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
From Coq Require Import Int63 PArray.
Open Scope array_scope.
(* Immediate values *)
Definition t1 : array nat := [| 3; 3; 3; 3 | 3 |].
Definition t2 := PArray.make 4 3.
Definition foo1 := (eq_refl : t1 = t2).
Definition foo2 := (eq_refl t1 <: t1 = t2).
Definition foo3 := (eq_refl t1 <<: t1 = t2).
Definition x1 := Eval compute in t2.
Definition foo4 := (eq_refl : x1 = t1).
Definition x2 := Eval cbn in t2.
Definition foo5 := (eq_refl : x2 = t1).
Definition partial1 := Eval lazy in @PArray.make.
Definition partial2 := Eval vm_compute in @PArray.make.
Definition partial3 := Eval native_compute in @PArray.make.
|
