From: Enrico Tassi Date: Wed, 2 Sep 2009 10:13:05 +0000 (+0000) Subject: CIC has no eta-reduction/expansion X-Git-Tag: make_still_working~3508 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=722bd96ca0e42f7ab4f6268ff6d4f667576b0b76;p=helm.git CIC has no eta-reduction/expansion --- diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index bc7e6f9ce..eb4b32ce3 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -346,12 +346,19 @@ ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1 | xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))))) ]. -ndefinition b8_to_recb8 : Πb.rec_byte8 b. - #b; - nletin K ≝ (b8_to_recb8_aux3 (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b)))); - nelim b in K:(%) ⊢ %; - #e1; #e2; nnormalize; #H; napply H. +(* +nlemma b8_to_recb8 : Πb.rec_byte8 b. + #b; nletin K ≝ (b8_to_recb8_aux3 + (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b)))); + ncases b in K; #e1; #e2; #K; napply K; nqed. +*) + +ndefinition b8_to_recb8 : Πb.rec_byte8 b ≝ + λb.match b with + [ mk_byte8 h l ⇒ + b8_to_recb8_aux3 + h l (b8_to_recb8_aux2 h (ex_to_recex h)) ]. (* ottali → esadecimali *) ndefinition b8_of_bit ≝