aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/ind.v
blob: 3af94c3b91a275f8d883563873448c9574323c8c (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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
Module Type SIG.
  Inductive w : Set :=
      A : w.
  Parameter f : w -> w.
End SIG.

Module M : SIG.
  Inductive w : Set :=
      A : w.
  Definition f x := match x with
                    | A => A
                    end.
End M.

Module N := M.

Check (N.f M.A).

(* Check use of equivalence on inductive types (bug #1242) *)

  Module Type ASIG.
  Inductive t : Set := a | b : t.
  Definition f := fun x => match x with a => true | b => false end.
  End ASIG.

  Module Type BSIG.
  Declare Module A : ASIG.
  Definition f := fun x => match x with A.a => true | A.b => false end.
  End BSIG.

  Module C (A : ASIG) (B : BSIG with Module A:=A).

  (* Check equivalence is considered in "case_info" *)
  Lemma test : forall x, A.f x = B.f x.
  intro x. unfold B.f, A.f.
  destruct x; reflexivity.
  Qed.

  (* Check equivalence is considered in pattern-matching *)
  Definition f (x : A.t) := match x with B.A.a => true | B.A.b => false end.

  End C.

(* Check subtyping of the context of parameters of the inductive types *)
(* Only the number of expected uniform parameters and the convertibility *)
(* of the inductive arities and constructors types are checked *)

Module Type S. Inductive I (x:=0) (y:nat): Set := c: x=y -> I y. End S.
Module P : S.  Inductive I (y':nat) (z:=y'): Set := c : 0=y' -> I y'. End P.