X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Fascii.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Fascii.ma;h=9cebb3317631478b1da89cc380d2856277211a97;hb=db235934efa41a0f38e79747f6db4f468367410b;hp=0000000000000000000000000000000000000000;hpb=b1c174cffd3c1d10383a52d63a6e662156fb0bb7;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii.ma b/helm/software/matita/contribs/ng_assembly/common/ascii.ma new file mode 100755 index 000000000..9cebb3317 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/ascii.ma @@ -0,0 +1,167 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ************************** *) +(* DEFINIZIONE ASCII MINIMALE *) +(* ************************** *) + +ninductive ascii : Type ≝ +(* numeri *) + ch_0: ascii +| ch_1: ascii +| ch_2: ascii +| ch_3: ascii +| ch_4: ascii +| ch_5: ascii +| ch_6: ascii +| ch_7: ascii +| ch_8: ascii +| ch_9: ascii + +(* simboli *) +| ch__: ascii + +(* maiuscole *) +| ch_A: ascii +| ch_B: ascii +| ch_C: ascii +| ch_D: ascii +| ch_E: ascii +| ch_F: ascii +| ch_G: ascii +| ch_H: ascii +| ch_I: ascii +| ch_J: ascii +| ch_K: ascii +| ch_L: ascii +| ch_M: ascii +| ch_N: ascii +| ch_O: ascii +| ch_P: ascii +| ch_Q: ascii +| ch_R: ascii +| ch_S: ascii +| ch_T: ascii +| ch_U: ascii +| ch_V: ascii +| ch_W: ascii +| ch_X: ascii +| ch_Y: ascii +| ch_Z: ascii + +(* minuscole *) +| ch_a: ascii +| ch_b: ascii +| ch_c: ascii +| ch_d: ascii +| ch_e: ascii +| ch_f: ascii +| ch_g: ascii +| ch_h: ascii +| ch_i: ascii +| ch_j: ascii +| ch_k: ascii +| ch_l: ascii +| ch_m: ascii +| ch_n: ascii +| ch_o: ascii +| ch_p: ascii +| ch_q: ascii +| ch_r: ascii +| ch_s: ascii +| ch_t: ascii +| ch_u: ascii +| ch_v: ascii +| ch_w: ascii +| ch_x: ascii +| ch_y: ascii +| ch_z: ascii. + +(* confronto fra ascii *) +ndefinition eq_ascii ≝ +λc,c':ascii.match c with + [ ch_0 ⇒ match c' with [ ch_0 ⇒ true | _ ⇒ false ] + | ch_1 ⇒ match c' with [ ch_1 ⇒ true | _ ⇒ false ] + | ch_2 ⇒ match c' with [ ch_2 ⇒ true | _ ⇒ false ] + | ch_3 ⇒ match c' with [ ch_3 ⇒ true | _ ⇒ false ] + | ch_4 ⇒ match c' with [ ch_4 ⇒ true | _ ⇒ false ] + | ch_5 ⇒ match c' with [ ch_5 ⇒ true | _ ⇒ false ] + | ch_6 ⇒ match c' with [ ch_6 ⇒ true | _ ⇒ false ] + | ch_7 ⇒ match c' with [ ch_7 ⇒ true | _ ⇒ false ] + | ch_8 ⇒ match c' with [ ch_8 ⇒ true | _ ⇒ false ] + | ch_9 ⇒ match c' with [ ch_9 ⇒ true | _ ⇒ false ] + | ch__ ⇒ match c' with [ ch__ ⇒ true | _ ⇒ false ] + | ch_A ⇒ match c' with [ ch_A ⇒ true | _ ⇒ false ] + | ch_B ⇒ match c' with [ ch_B ⇒ true | _ ⇒ false ] + | ch_C ⇒ match c' with [ ch_C ⇒ true | _ ⇒ false ] + | ch_D ⇒ match c' with [ ch_D ⇒ true | _ ⇒ false ] + | ch_E ⇒ match c' with [ ch_E ⇒ true | _ ⇒ false ] + | ch_F ⇒ match c' with [ ch_F ⇒ true | _ ⇒ false ] + | ch_G ⇒ match c' with [ ch_G ⇒ true | _ ⇒ false ] + | ch_H ⇒ match c' with [ ch_H ⇒ true | _ ⇒ false ] + | ch_I ⇒ match c' with [ ch_I ⇒ true | _ ⇒ false ] + | ch_J ⇒ match c' with [ ch_J ⇒ true | _ ⇒ false ] + | ch_K ⇒ match c' with [ ch_K ⇒ true | _ ⇒ false ] + | ch_L ⇒ match c' with [ ch_L ⇒ true | _ ⇒ false ] + | ch_M ⇒ match c' with [ ch_M ⇒ true | _ ⇒ false ] + | ch_N ⇒ match c' with [ ch_N ⇒ true | _ ⇒ false ] + | ch_O ⇒ match c' with [ ch_O ⇒ true | _ ⇒ false ] + | ch_P ⇒ match c' with [ ch_P ⇒ true | _ ⇒ false ] + | ch_Q ⇒ match c' with [ ch_Q ⇒ true | _ ⇒ false ] + | ch_R ⇒ match c' with [ ch_R ⇒ true | _ ⇒ false ] + | ch_S ⇒ match c' with [ ch_S ⇒ true | _ ⇒ false ] + | ch_T ⇒ match c' with [ ch_T ⇒ true | _ ⇒ false ] + | ch_U ⇒ match c' with [ ch_U ⇒ true | _ ⇒ false ] + | ch_V ⇒ match c' with [ ch_V ⇒ true | _ ⇒ false ] + | ch_W ⇒ match c' with [ ch_W ⇒ true | _ ⇒ false ] + | ch_X ⇒ match c' with [ ch_X ⇒ true | _ ⇒ false ] + | ch_Y ⇒ match c' with [ ch_Y ⇒ true | _ ⇒ false ] + | ch_Z ⇒ match c' with [ ch_Z ⇒ true | _ ⇒ false ] + | ch_a ⇒ match c' with [ ch_a ⇒ true | _ ⇒ false ] + | ch_b ⇒ match c' with [ ch_b ⇒ true | _ ⇒ false ] + | ch_c ⇒ match c' with [ ch_c ⇒ true | _ ⇒ false ] + | ch_d ⇒ match c' with [ ch_d ⇒ true | _ ⇒ false ] + | ch_e ⇒ match c' with [ ch_e ⇒ true | _ ⇒ false ] + | ch_f ⇒ match c' with [ ch_f ⇒ true | _ ⇒ false ] + | ch_g ⇒ match c' with [ ch_g ⇒ true | _ ⇒ false ] + | ch_h ⇒ match c' with [ ch_h ⇒ true | _ ⇒ false ] + | ch_i ⇒ match c' with [ ch_i ⇒ true | _ ⇒ false ] + | ch_j ⇒ match c' with [ ch_j ⇒ true | _ ⇒ false ] + | ch_k ⇒ match c' with [ ch_k ⇒ true | _ ⇒ false ] + | ch_l ⇒ match c' with [ ch_l ⇒ true | _ ⇒ false ] + | ch_m ⇒ match c' with [ ch_m ⇒ true | _ ⇒ false ] + | ch_n ⇒ match c' with [ ch_n ⇒ true | _ ⇒ false ] + | ch_o ⇒ match c' with [ ch_o ⇒ true | _ ⇒ false ] + | ch_p ⇒ match c' with [ ch_p ⇒ true | _ ⇒ false ] + | ch_q ⇒ match c' with [ ch_q ⇒ true | _ ⇒ false ] + | ch_r ⇒ match c' with [ ch_r ⇒ true | _ ⇒ false ] + | ch_s ⇒ match c' with [ ch_s ⇒ true | _ ⇒ false ] + | ch_t ⇒ match c' with [ ch_t ⇒ true | _ ⇒ false ] + | ch_u ⇒ match c' with [ ch_u ⇒ true | _ ⇒ false ] + | ch_v ⇒ match c' with [ ch_v ⇒ true | _ ⇒ false ] + | ch_w ⇒ match c' with [ ch_w ⇒ true | _ ⇒ false ] + | ch_x ⇒ match c' with [ ch_x ⇒ true | _ ⇒ false ] + | ch_y ⇒ match c' with [ ch_y ⇒ true | _ ⇒ false ] + | ch_z ⇒ match c' with [ ch_z ⇒ true | _ ⇒ false ] + ].