helm/software/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 Π_.Π_.?.