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 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_data".
17 include "../../library/datatypes/constructors.ma".
18 include "../../library/datatypes/bool.ma".
19 include "domain_defs.ma".
21 (* QUANTIFICATION DOMAINS
22 - Here we define some useful domains based on data types
25 definition DBool : Domain \def
26 mk_Domain (mk_Class bool (true_f ?) (eq ?)).
28 definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
31 [ false \Rightarrow c0
35 definition DVoid : Domain \def
36 mk_Domain (mk_Class void (true_f ?) (eq ?)).
38 definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def
40 match v in void with [].