2) several eliminiation principles and projections are now automatically generated
nelim b2;
nnormalize;
#H;
- ##[ ##2: napply (False_ind (λx.P) ?);
+ ##[ ##2: napply (False_ind (λx.?) ?);
(* perche' non napply (False_ind ??); !!! *)
nchange with (match true with [ true ⇒ False | false ⇒ True]);
nrewrite > H;
nnormalize;
napply I
- ##| ##3: napply (False_ind (λx.P) ?);
+ ##| ##3: napply (False_ind (λx.?) ?);
(* perche' non napply (False_ind ??); !!! *)
nchange with (match true with [ true ⇒ False | false ⇒ True]);
nrewrite < H;
b8l: exadecim
}.
-ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
+(*ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
λP:byte8 → Prop.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
ndefinition b8h ≝ λb:byte8.match b with [ mk_byte8 x _ ⇒ x ].
-ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].
+ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].*)
(* \langle \rangle *)
notation "〈x,y〉" non associative with precedence 80
None : option A
| Some : A → option A.
-ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
+(*ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
λA:Type.λP:option A → Prop.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
ndefinition option_rect : ΠA:Type.ΠP:option A → Type.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
λA:Type.λP:option A → Type.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
- match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
+ match op with [ None ⇒ p | Some (a:A) ⇒ f a ].*)
ndefinition eq_option ≝
λT.λop1,op2:option T.λf:T → T → bool.
(* *)
(* ********************************************************************** *)
-universe constraint Type[0] < Type[1].
-universe constraint Type[1] < Type[2].
-universe constraint CProp[0] < CProp[1].
-universe constraint Type[0] ≤ CProp[0].
-universe constraint CProp[0] ≤ Type[0].
-universe constraint Type[1] ≤ CProp[1].
-universe constraint CProp[1] ≤ Type[1].
-
+universe constraint Type[0] < Type[1].
\ No newline at end of file
w16l: byte8
}.
-ndefinition word16_ind : ΠP:word16 → Prop.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
+(*ndefinition word16_ind : ΠP:word16 → Prop.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
λP:word16 → Prop.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
ndefinition w16h ≝ λw:word16.match w with [ mk_word16 x _ ⇒ x ].
-ndefinition w16l ≝ λw:word16.match w with [ mk_word16 _ x ⇒ x ].
+ndefinition w16l ≝ λw:word16.match w with [ mk_word16 _ x ⇒ x ].*)
(* \langle \rangle *)
notation "〈x:y〉" non associative with precedence 80
w32l: word16
}.
-ndefinition word32_ind : ΠP:word32 → Prop.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
+(*ndefinition word32_ind : ΠP:word32 → Prop.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
λP:word32 → Prop.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
ndefinition w32h ≝ λdw:word32.match dw with [ mk_word32 x _ ⇒ x ].
-ndefinition w32l ≝ λdw:word32.match dw with [ mk_word32 _ x ⇒ x ].
+ndefinition w32l ≝ λdw:word32.match dw with [ mk_word32 _ x ⇒ x ].*)
(* \langle \rangle *)
notation "〈x.y〉" non associative with precedence 80
| 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_rec
- : ΠP:ascii → Set.
- 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 → Set.
-λ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__ →
ndefinition ascii_destruct1 : Πc2.ΠP:Prop.ch_0 = c2 → match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##1: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ninductive aux_strId_type : Type ≝
STR_ID: aux_str_type → nat → aux_strId_type.
-ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
+(*ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
match a with [ STR_ID l n ⇒ f l n ].
ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].
+ match a with [ STR_ID l n ⇒ f l n ].*)
(* getter *)
ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
| ne_nil: A → ne_list A
| ne_cons: A → ne_list A → ne_list A.
-nlet rec ne_list_ind (A:Type) (P:ne_list A → Prop) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
+(*nlet rec ne_list_ind (A:Type) (P:ne_list A → Prop) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_ind A P f f1 t) ].
nlet rec ne_list_rec (A:Type) (P:ne_list A → Set) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rec A P f f1 t) ].
nlet rec ne_list_rect (A:Type) (P:ne_list A → Type) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
- match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rect A P f f1 t) ].
+ match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rect A P f f1 t) ].*)
(* append *)
nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
match l
return λl:list T.isnot_empty_list T l → ne_list T
with
- [ nil ⇒ λp:isnot_empty_list T (nil T).False_rect ? p
+ [ nil ⇒ λp:isnot_empty_list T (nil T).False_rect_Type0 ? p
| cons h t ⇒ λp:isnot_empty_list T (cons T h t).
match list_to_neList_aux T t with
[ None ⇒ «£h»
[ nil ⇒ λl2.match l2 return λl2.len_list T1 [] = len_list T1 l2 → T2 with
[ nil ⇒ λp:len_list T1 [] = len_list T1 [].acc
| cons h t ⇒ λp:len_list T1 [] = len_list T1 (h::t).
- False_rect ? (fold_right_list2_aux1 T1 h t p)
+ False_rect_Type0 ? (fold_right_list2_aux1 T1 h t p)
]
| cons h t ⇒ λl2.match l2 return λl2.len_list T1 (h::t) = len_list T1 l2 → T2 with
[ nil ⇒ λp:len_list T1 (h::t) = len_list T1 [].
- False_rect ? (fold_right_list2_aux2 T1 h t p)
+ False_rect_Type0 ? (fold_right_list2_aux2 T1 h t p)
| cons h' t' ⇒ λp:len_list T1 (h::t) = len_list T1 (h'::t').
f h h' (fold_right_list2 T1 T2 f acc t t' (fold_right_list2_aux3 T1 h h' t t' p))
]
[ ne_nil h' ⇒ λp:len_neList T1 «£h» = len_neList T1 «£h'».
f h h' acc
| ne_cons h' t' ⇒ λp:len_neList T1 «£h» = len_neList T1 (h'§§t').
- False_rect ? (fold_right_neList2_aux1 T1 h h' t' p)
+ False_rect_Type0 ? (fold_right_neList2_aux1 T1 h h' t' p)
]
| ne_cons h t ⇒ λl2.match l2 return λl2.len_neList T1 (h§§t) = len_neList T1 l2 → T2 with
[ ne_nil h' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 «£h'».
- False_rect ? (fold_right_neList2_aux2 T1 h h' t p)
+ False_rect_Type0 ? (fold_right_neList2_aux2 T1 h h' t p)
| ne_cons h' t' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 (h'§§t').
f h h' (fold_right_neList2 T1 T2 f acc t t' (fold_right_neList2_aux3 T1 h h' t t' p))
]
projects / helm.git / commitdiff