| ch_y: ascii
| ch_z: ascii.
-(*ndefinition ascii_ind
- : ΠP:ascii → Prop.
- P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
- P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
- P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V →
- P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g →
- P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r →
- P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝
-λP:ascii → Prop.
-λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9.
-λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H.
-λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q.
-λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z.
-λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i.
-λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r.
-λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii.
- match a with
- [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7
- | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15
- | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23
- | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31
- | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39
- | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
- | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
- | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
-
-ndefinition ascii_rect
- : ΠP:ascii → Type.
- P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
- P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
- P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V →
- P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g →
- P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r →
- P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝
-λP:ascii → Type.
-λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9.
-λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H.
-λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q.
-λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z.
-λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i.
-λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r.
-λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii.
- match a with
- [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7
- | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15
- | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23
- | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31
- | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39
- | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
- | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
- | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
-*)
(* confronto fra ascii *)
ndefinition eq_ascii ≝
λc,c':ascii.match c with
projects / helm.git / blobdiff