From 722bd96ca0e42f7ab4f6268ff6d4f667576b0b76 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Sep 2009 10:13:05 +0000 Subject: [PATCH] CIC has no eta-reduction/expansion --- .../matita/contribs/ng_assembly/num/byte8.ma | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) 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 ≝ -- 2.39.2