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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "utility/ascii.ma".
24 include "freescale/theory.ma".
25 include "freescale/nat.ma".
27 (* ************************ *)
28 (* MANIPOLAZIONE DI STRINGA *)
29 (* ************************ *)
32 ndefinition aux_str_type ≝ list ascii.
35 nlet rec eq_str (str,str':aux_str_type) ≝
37 [ nil ⇒ match str' with
40 | cons h t ⇒ match str' with
42 | cons h' t' ⇒ (eq_ascii h h')⊗(eq_str t t')
51 ninductive aux_strId_type : Type ≝
52 STR_ID: aux_str_type → nat → aux_strId_type.
54 ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
55 λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
56 match a with [ STR_ID l n ⇒ f l n ].
58 ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
59 λP:aux_strId_type → Set.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
60 match a with [ STR_ID l n ⇒ f l n ].
62 ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
63 λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
64 match a with [ STR_ID l n ⇒ f l n ].
67 ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
68 ndefinition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
71 ndefinition eq_strId ≝
72 λsid,sid':aux_strId_type.(eq_str (get_name_strId sid) (get_name_strId sid'))⊗(eq_nat (get_id_strId sid) (get_id_strId sid')).