1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "arithmetics/nat.ma".
16 include "basics/bool.ma".
17 include "basics/lists/listb.ma".
19 inductive coerc : Type[0] ≝
21 | CBool : bool → coerc.
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 ⇒
31 inductive type : Type[0] ≝
36 definition denotation_sem ≝ λn.
40 (* Funzione di equivalenza tra tipi *)
41 definition eqb_type ≝ λa,b. eqb (denotation_sem a) (denotation_sem b).
42 definition getType : coerc → type ≝