aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4251.v
blob: 66343d66717874bd9535d5b41b78855ff35386f2 (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).