blob: f112e7b4d5947c55037e8fdbd492dea9758e2a8c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Inductive array : Type -> Type :=
| carray : forall A, array A.
Inductive Mtac : Type -> Prop :=
| bind : forall {A B}, Mtac A -> (A -> Mtac B) -> Mtac B
| array_make : forall {A}, A -> Mtac (array A).
Definition Ref := array.
Definition ref : forall {A}, A -> Mtac (Ref A) :=
fun A x=> array_make x.
Check array Type.
Check fun A : Type => Ref A.
Definition abs_val (a : Type) :=
bind (ref a) (fun r : array Type => array_make tt).
|
