Changeset 279 for Deliverables/D4.1/Matita
 Timestamp:
 Nov 24, 2010, 5:19:38 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Assembly.ma
r272 r279 1 1 include "ASM.ma". 2 3 (*4 ndefinition from_addressing_mode_tag ≝5 λT:Type[0].λt:addressing_mode_tag.6 match t with7 [ direct ⇒ Byte → T8  indirect ⇒ Bit → T9  ext_indirect ⇒ Bit → T10  register ⇒ Bit → Bit → Bit → T11  acc_a ⇒ T12  acc_b ⇒ T13  dptr ⇒ T14  data ⇒ Byte → T15  data16 ⇒ Word → T16  acc_dptr ⇒ T17  acc_pc ⇒ T18  ext_indirect_dptr ⇒ T19  indirect_dptr ⇒ T20  carry ⇒ T21  bit_addr ⇒ Bit → T22  n_bit_addr ⇒ Bit → T23  relative ⇒ Byte → T24  addr11 ⇒ Word11 → T25  addr16 ⇒ Word → T ].26 *)27 (*28 nlet rec elim_addr (T:addressing_mode → Type[0]) n l on l29 : subaddressing_mode n l → Type[0] ≝30 match l31 return λm.λl:Vector addressing_mode_tag m.32 ∀proof:m = S n.33 subaddressing_mode n (match proof with [refl ⇒ l]) → Type[0] with34 [ Empty ⇒ λK.λ_.Nat35  Cons o he tl ⇒ λK.λv.Nat(*36 match o37 return λy.∀p:S y = S n.38 subaddressing_mode y39 (v⌈Vector addressing_mode_tag (S y) ↦ Vector addressing_mode_tag (S n)⌉)40 → Type[0]41 with42 [ Z ⇒ λK.λv.(? : Type[0])43  S p ⇒ λK.λv.(? : Type[0])44 ]*)45 ] (?: S n = S n).46 ##[##1: @47  ndestruct48 ##7: //49  normalize;50 51 nlet rec elim_addr n (v: Vector addressing_mode_tag (S n)) on v52 : subaddressing_mode n v Type[0]53 ≝54 match v return λx.λ_.x = S n. Type[0] with55 [ Empty ⇒ λK.⊥56  Cons o he tl ⇒ λK.57 match o with58 [ Z ⇒59  S m ⇒60 ]61 ] (? : S n = S n).62 *)63 64 notation "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"65 with precedence 1066 for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.67 68 ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).69 2 70 3 ndefinition assembly1 ≝ 
Deliverables/D4.1/Matita/Cartesian.ma
r268 r279 8 8 interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r). 9 9 interpretation "Cartesian" 'product A B = (Cartesian A B). 10 11 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 12 with precedence 10 13 for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }. 14 15 (*ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).*) 16
Note: See TracChangeset
for help on using the changeset viewer.