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/word16.ma".
25 (* raggruppamento di byte e word in un tipo unico *)
26 ninductive byte8_or_word16 : Type ≝
27 Byte: byte8 → byte8_or_word16
28 | Word: word16 → byte8_or_word16.
30 ndefinition eq_b8w16 ≝
31 λbw1,bw2:byte8_or_word16.
33 [ Byte b1 ⇒ match bw2 with [ Byte b2 ⇒ eqc ? b1 b2 | Word _ ⇒ false ]
34 | Word w1 ⇒ match bw2 with [ Byte _ ⇒ false | Word w2 ⇒ eqc ? w1 w2 ]