freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
index 53d798b35114664e599021fb7c0521ee8e11c56b..efc8d9aab9690b7e5075725421714299567cf82a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
@@ -32,21 +32,6 @@ nrecord word16 : Type ≝
  w16l: byte8
  }.
 
-(*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 ].
-
-ndefinition word16_rec : ΠP:word16 → Set.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
-λP:word16 → Set.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
- match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
-
-ndefinition word16_rect : ΠP:word16 → Type.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
-λP:word16 → Type.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
- 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 ].*)
-
 (* \langle \rangle *)
 notation "〈x:y〉" non associative with precedence 80
  for @{ 'mk_word16 $x $y }.