aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4161.v
blob: d2003ab1f0017a7b68dd4d0c0e49d991ffe4250f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

    (* Inductive t : Type -> Type := *)
    (* | Just : forall (A : Type), t A -> t A. *)

    (* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *)
    (*   match x in t A return t (A + unit) with *)
    (*   | Just T x => @test T x *)
    (*   end. *)


    Definition Type1 := Type.
Definition Type2 := Type.
Definition cast (x:Type2) := x:Type1.
Axiom f: Type2 -> Prop.
Definition A :=
 let T := fun A:Type1 => _ in
 fun A':Type2 =>
 eq_refl : T A' = f A' :> Prop.
(* Type2 <= Type1... f A -> Type1 <= Type2 *)

Inductive t : Type -> Type :=
    | Just : forall (A : Type), t A -> t A.

Fixpoint test {A : Type} (x : t A) : t (A + unit) :=
  match x in t A with
  | Just B x => @test B x
  end.