]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/common/ascii.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / ng_assembly / common / ascii.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/bool.ma".
24
25 (* ************************** *)
26 (* DEFINIZIONE ASCII MINIMALE *)
27 (* ************************** *)
28
29 ninductive ascii : Type ≝
30 (* numeri *)  
31   ch_0: ascii
32 | ch_1: ascii
33 | ch_2: ascii
34 | ch_3: ascii
35 | ch_4: ascii
36 | ch_5: ascii
37 | ch_6: ascii
38 | ch_7: ascii
39 | ch_8: ascii
40 | ch_9: ascii
41
42 (* simboli *)
43 | ch__: ascii
44
45 (* maiuscole *)
46 | ch_A: ascii
47 | ch_B: ascii
48 | ch_C: ascii
49 | ch_D: ascii
50 | ch_E: ascii
51 | ch_F: ascii
52 | ch_G: ascii
53 | ch_H: ascii
54 | ch_I: ascii
55 | ch_J: ascii
56 | ch_K: ascii
57 | ch_L: ascii
58 | ch_M: ascii
59 | ch_N: ascii
60 | ch_O: ascii
61 | ch_P: ascii
62 | ch_Q: ascii
63 | ch_R: ascii
64 | ch_S: ascii
65 | ch_T: ascii
66 | ch_U: ascii
67 | ch_V: ascii
68 | ch_W: ascii
69 | ch_X: ascii
70 | ch_Y: ascii
71 | ch_Z: ascii
72
73 (* minuscole *)
74 | ch_a: ascii
75 | ch_b: ascii
76 | ch_c: ascii
77 | ch_d: ascii
78 | ch_e: ascii
79 | ch_f: ascii
80 | ch_g: ascii
81 | ch_h: ascii
82 | ch_i: ascii
83 | ch_j: ascii
84 | ch_k: ascii
85 | ch_l: ascii
86 | ch_m: ascii
87 | ch_n: ascii
88 | ch_o: ascii
89 | ch_p: ascii
90 | ch_q: ascii
91 | ch_r: ascii
92 | ch_s: ascii
93 | ch_t: ascii
94 | ch_u: ascii
95 | ch_v: ascii
96 | ch_w: ascii
97 | ch_x: ascii
98 | ch_y: ascii
99 | ch_z: ascii.
100
101 (* confronto fra ascii *)
102 ndefinition eq_ascii ≝
103 λc,c':ascii.match c with
104  [ ch_0 ⇒ match c' with [ ch_0 ⇒ true | _ ⇒ false ]
105  | ch_1 ⇒ match c' with [ ch_1 ⇒ true | _ ⇒ false ]
106  | ch_2 ⇒ match c' with [ ch_2 ⇒ true | _ ⇒ false ]
107  | ch_3 ⇒ match c' with [ ch_3 ⇒ true | _ ⇒ false ]
108  | ch_4 ⇒ match c' with [ ch_4 ⇒ true | _ ⇒ false ]
109  | ch_5 ⇒ match c' with [ ch_5 ⇒ true | _ ⇒ false ]
110  | ch_6 ⇒ match c' with [ ch_6 ⇒ true | _ ⇒ false ]
111  | ch_7 ⇒ match c' with [ ch_7 ⇒ true | _ ⇒ false ]
112  | ch_8 ⇒ match c' with [ ch_8 ⇒ true | _ ⇒ false ]
113  | ch_9 ⇒ match c' with [ ch_9 ⇒ true | _ ⇒ false ]
114  | ch__ ⇒ match c' with [ ch__ ⇒ true | _ ⇒ false ]
115  | ch_A ⇒ match c' with [ ch_A ⇒ true | _ ⇒ false ]
116  | ch_B ⇒ match c' with [ ch_B ⇒ true | _ ⇒ false ]
117  | ch_C ⇒ match c' with [ ch_C ⇒ true | _ ⇒ false ]
118  | ch_D ⇒ match c' with [ ch_D ⇒ true | _ ⇒ false ]
119  | ch_E ⇒ match c' with [ ch_E ⇒ true | _ ⇒ false ]
120  | ch_F ⇒ match c' with [ ch_F ⇒ true | _ ⇒ false ]
121  | ch_G ⇒ match c' with [ ch_G ⇒ true | _ ⇒ false ]
122  | ch_H ⇒ match c' with [ ch_H ⇒ true | _ ⇒ false ]
123  | ch_I ⇒ match c' with [ ch_I ⇒ true | _ ⇒ false ]
124  | ch_J ⇒ match c' with [ ch_J ⇒ true | _ ⇒ false ]
125  | ch_K ⇒ match c' with [ ch_K ⇒ true | _ ⇒ false ]
126  | ch_L ⇒ match c' with [ ch_L ⇒ true | _ ⇒ false ]
127  | ch_M ⇒ match c' with [ ch_M ⇒ true | _ ⇒ false ]
128  | ch_N ⇒ match c' with [ ch_N ⇒ true | _ ⇒ false ]
129  | ch_O ⇒ match c' with [ ch_O ⇒ true | _ ⇒ false ]
130  | ch_P ⇒ match c' with [ ch_P ⇒ true | _ ⇒ false ]
131  | ch_Q ⇒ match c' with [ ch_Q ⇒ true | _ ⇒ false ]
132  | ch_R ⇒ match c' with [ ch_R ⇒ true | _ ⇒ false ]
133  | ch_S ⇒ match c' with [ ch_S ⇒ true | _ ⇒ false ]
134  | ch_T ⇒ match c' with [ ch_T ⇒ true | _ ⇒ false ]
135  | ch_U ⇒ match c' with [ ch_U ⇒ true | _ ⇒ false ]
136  | ch_V ⇒ match c' with [ ch_V ⇒ true | _ ⇒ false ]
137  | ch_W ⇒ match c' with [ ch_W ⇒ true | _ ⇒ false ]
138  | ch_X ⇒ match c' with [ ch_X ⇒ true | _ ⇒ false ]
139  | ch_Y ⇒ match c' with [ ch_Y ⇒ true | _ ⇒ false ]
140  | ch_Z ⇒ match c' with [ ch_Z ⇒ true | _ ⇒ false ]
141  | ch_a ⇒ match c' with [ ch_a ⇒ true | _ ⇒ false ]
142  | ch_b ⇒ match c' with [ ch_b ⇒ true | _ ⇒ false ]
143  | ch_c ⇒ match c' with [ ch_c ⇒ true | _ ⇒ false ]
144  | ch_d ⇒ match c' with [ ch_d ⇒ true | _ ⇒ false ]
145  | ch_e ⇒ match c' with [ ch_e ⇒ true | _ ⇒ false ]
146  | ch_f ⇒ match c' with [ ch_f ⇒ true | _ ⇒ false ]
147  | ch_g ⇒ match c' with [ ch_g ⇒ true | _ ⇒ false ]
148  | ch_h ⇒ match c' with [ ch_h ⇒ true | _ ⇒ false ]
149  | ch_i ⇒ match c' with [ ch_i ⇒ true | _ ⇒ false ]
150  | ch_j ⇒ match c' with [ ch_j ⇒ true | _ ⇒ false ]
151  | ch_k ⇒ match c' with [ ch_k ⇒ true | _ ⇒ false ]
152  | ch_l ⇒ match c' with [ ch_l ⇒ true | _ ⇒ false ]
153  | ch_m ⇒ match c' with [ ch_m ⇒ true | _ ⇒ false ]
154  | ch_n ⇒ match c' with [ ch_n ⇒ true | _ ⇒ false ]
155  | ch_o ⇒ match c' with [ ch_o ⇒ true | _ ⇒ false ]
156  | ch_p ⇒ match c' with [ ch_p ⇒ true | _ ⇒ false ]
157  | ch_q ⇒ match c' with [ ch_q ⇒ true | _ ⇒ false ]
158  | ch_r ⇒ match c' with [ ch_r ⇒ true | _ ⇒ false ]
159  | ch_s ⇒ match c' with [ ch_s ⇒ true | _ ⇒ false ]
160  | ch_t ⇒ match c' with [ ch_t ⇒ true | _ ⇒ false ]
161  | ch_u ⇒ match c' with [ ch_u ⇒ true | _ ⇒ false ]
162  | ch_v ⇒ match c' with [ ch_v ⇒ true | _ ⇒ false ]
163  | ch_w ⇒ match c' with [ ch_w ⇒ true | _ ⇒ false ]
164  | ch_x ⇒ match c' with [ ch_x ⇒ true | _ ⇒ false ]
165  | ch_y ⇒ match c' with [ ch_y ⇒ true | _ ⇒ false ]
166  | ch_z ⇒ match c' with [ ch_z ⇒ true | _ ⇒ false ]
167  ].