matita/matita/projdat/basic_type.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 "arithmetics/nat.ma".
  16 include "basics/bool.ma".
  17 include "basics/lists/listb.ma".
  18
  19 inductive coerc : Type[0] ≝
  20   | CNat : nat → coerc
  21   | CBool : bool → coerc.
  22
  23 definition eq_c ≝ λa,b. match a with
  24   [ CNat n ⇒ (match b with [ CNat m ⇒ eqb n m | _ ⇒ false ])
  25   | CBool x ⇒ (match b with [ CBool y ⇒
  26                              beqb x y
  27                             | _ ⇒ false]
  28               )
  29   ].
  30
  31 inductive type : Type[0] ≝
  32   | Nat : type
  33   | Bool: type.
  34
  35
  36 definition denotation_sem ≝ λn.
  37   match n with
  38   [ Nat ⇒ 1
  39   | Bool ⇒ 2].
  40 (* Funzione di equivalenza tra tipi *)
  41 definition eqb_type ≝ λa,b. eqb (denotation_sem a) (denotation_sem b).
  42 definition getType : coerc → type ≝
  43 λ gt. match gt with
  44   [ CNat _ ⇒ Nat
  45   | CBool _ ⇒ Bool].
  46
  47
  48