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 ninductive list (A : Type) : Type ≝
  18  | nil : list A
  19  | cons : A → list A → list A.
  20
  21 naxiom T : Type.
  22 naxiom S : Type.
  23 naxiom c : list T → list S.
  24
  25 ncoercion foo : ∀_l:list T. list S ≝ c
  26   on _l : list T
  27   to      list ?.
  28
  29 naxiom P : list S → Prop.
  30
  31 ndefinition t1 ≝ ∀x:list T.P x → ?. ##[ napply Prop; ##] nqed.
  32
  33 ncoercion bar : ∀_l:list T. S → S ≝ λ_.λx.x
  34   on _l : list T
  35   to      Π_.?.
  36
  37 naxiom Q : (S → S) → Prop.
  38
  39 ndefinition t2 ≝ ∀x:list T.Q x → ?. ##[ napply Prop; ##] nqed.
  40
  41
  42