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 }.