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 "Domain/defs.ma".
17 (* QUANTIFICATION DOMAINS
18 - Here we define some useful domains based on data types.
21 definition DBool: Domain ≝
23 mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
26 definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
29 [ false \Rightarrow c0
33 definition DVoid: Domain ≝
35 mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
38 definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def
40 match v in void with [].