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 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/bool.ma".
25 (* ************************* *)
26 (* dimensioni degli elementi *)
27 (* ************************* *)
29 (* usato per definire nell'ast *)
30 ninductive ast_base_type : Type ≝
31 AST_BASE_TYPE_BYTE8: ast_base_type
32 | AST_BASE_TYPE_WORD16: ast_base_type
33 | AST_BASE_TYPE_WORD32: ast_base_type.
36 ndefinition forall_astbasetype ≝ λP.
37 P AST_BASE_TYPE_BYTE8 ⊗
38 P AST_BASE_TYPE_WORD16 ⊗
39 P AST_BASE_TYPE_WORD32.
41 ndefinition eq_astbasetype ≝
42 λt1,t2:ast_base_type.match t1 with
43 [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
44 | AST_BASE_TYPE_WORD16 ⇒ match t2 with [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
45 | AST_BASE_TYPE_WORD32 ⇒ match t2 with [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]