freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / byte8.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma b/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
index ed4a47ea3d0f79e4abef19763c856320f34da29b..896bf6e66a3f54bab329d751a7bd39cc6a8a193c 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
@@ -32,21 +32,6 @@ nrecord byte8 : Type ≝
  b8l: exadecim
  }.
 
-(*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 ].
-
-ndefinition byte8_rec : ΠP:byte8 → Set.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
-λP:byte8 → Set.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
- match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
-
-ndefinition byte8_rect : ΠP:byte8 → Type.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
-λP:byte8 → Type.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
- 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 ].*)
-
 (* \langle \rangle *)
 notation "〈x,y〉" non associative with precedence 80
  for @{ 'mk_byte8 $x $y }.