]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/tests/ng_coercions.ma
update in basic_2
[helm.git] / matitaB / matita / tests / ng_coercions.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ng_pts.ma".
16
17 (* easy *)
18 naxiom T : Type.
19 naxiom S : Type.
20 naxiom R : Type.
21 naxiom U : Type.
22 naxiom c : T → S.
23 naxiom c1 : S → R.
24 naxiom c2 : R → U.
25
26 ncoercion foo1 : ∀_t:T.S ≝ c on _t : T to S.
27 ncoercion foo2 : ∀_r:R.U ≝ c2 on _r : R to U.
28 ncoercion foo3 : ∀_s:S.R ≝ c1 on _s : S to R.
29
30 (* another *)
31
32 naxiom nat : Type.
33 naxiom A : nat → Type. 
34 naxiom B : nat → Type.
35 naxiom C : nat → Type.
36 naxiom D : nat → Type.
37 naxiom a :  ∀n:nat. A n → B n.
38 naxiom a1 : ∀n:nat. B n → C n.
39 naxiom a2 : ∀n:nat. C n → D n.
40
41 ncoercion foo1 : ∀n:nat. ∀_a:A n. B n ≝ a  on _a : A ? to B ?.
42 ncoercion foo2 : ∀n:nat. ∀_c:C n. D n ≝ a2 on _c : C ? to D ?.
43 ncoercion foo3 : ∀n:nat. ∀_b:B n. C n ≝ a1 on _b : B ? to C ?.
44
45 naxiom cx : ∀n,m:nat. B n → C m.
46
47 ncoercion foo3 : ∀n,m:nat. ∀_b:B n. C m ≝ cx on _b : B ? to C ?.
48
49 naxiom Suc : nat → nat.
50 naxiom cs : ∀n:nat. B n → C (Suc n).
51
52 ncoercion foo3 : ∀n:nat. ∀_b:B n. C (Suc n) ≝ cs on _b : B ? to C ?.
53
54 (* funclass *)
55 naxiom Y : Type.
56 naxiom W : Type.
57 naxiom X : Type.
58 naxiom f : Y → W.
59 naxiom g : W → X → X → X.
60
61 ncoercion foo : ∀_y:Y. W ≝ f on _y : Y to W. 
62 ncoercion foo : ∀_w:W. X → X → X ≝ g on _w : W to Π_.Π_.?.