--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+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 ]
+ ].
projects / helm.git / blobdiff