Changeset 362 for Deliverables


Ignore:
Timestamp:
Dec 2, 2010, 11:53:49 AM (9 years ago)
Author:
sacerdot
Message:

Less ambiguous definitions.

Location:
Deliverables/D4.1/Matita
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r357 r362  
    2424(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2525
     26(*
    2627ndefinition get_index_bv ≝
    2728  λn: Nat.
     
    2930  λm: Nat.
    3031  λp: m < n.
    31     get_index Bool n b m p.
     32    get_index_bv Bool n b m p.
    3233   
    3334interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
     
    4647  λm: Nat.
    4748    drop Bool n b m.
     49*)
    4850
    4951(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    5153(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    5254
    53 ndefinition zero ≝
    54   λn: Nat.
    55     ((replicate Bool n false): BitVector n).
    56    
    57 ndefinition max ≝
    58   λn: Nat.
    59     ((replicate Bool n true): BitVector n).
    60    
     55ndefinition zero: ∀n:Nat. BitVector n ≝
     56  λn: Nat. replicate Bool n false.
     57   
     58ndefinition max: ∀n:Nat. BitVector n ≝
     59  λn: Nat. replicate Bool n true.
     60
     61(*
    6162ndefinition append ≝
    6263  λm, n: Nat.
     
    6465  λc: BitVector n.
    6566    append Bool m n b c.
    66    
     67*)
     68 
    6769ndefinition pad ≝
    6870  λm, n: Nat.
     
    7577(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    7678
     79(*
    7780ndefinition reverse ≝
    7881  λn: Nat.
     
    8487  λb: BitVector n.
    8588    length Bool n b.
     89*)
    8690
    8791(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    126130(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    127131
     132(*
    128133ndefinition rotate_left_bv ≝
    129134  λn, m: Nat.
     
    147152  λc: Bool.
    148153    shift_right Bool n m b c.
    149    
     154*)
     155 
    150156(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    151157(* Conversions to and from lists and natural numbers.                         *)
    152158(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    153159
     160(*
    154161ndefinition list_of_bitvector ≝
    155162  λn: Nat.
     
    160167  λl: List Bool.
    161168    vector_of_list Bool l.
     169*)
    162170
    163171nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝
     
    194202  let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in
    195203  let size ≝ length ? biglist in
    196   let bitvector ≝ bitvector_of_list biglist in
     204  let bitvector ≝ vector_of_list ? biglist in
    197205  let difference ≝ n - size in
    198206   less_than_or_equal_b_elim …
  • Deliverables/D4.1/Matita/Interpret.ma

    r358 r362  
    1919            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    2020                                                   (get_arg_8 s false addr2) false in
    21             let cy_flag ≝ get_index … flags Z ? in
    22             let ac_flag ≝ get_index … flags one ? in
    23             let ov_flag ≝ get_index … flags two ? in
     21            let cy_flag ≝ get_index_v … flags Z ? in
     22            let ac_flag ≝ get_index_v … flags one ? in
     23            let ov_flag ≝ get_index_v … flags two ? in
    2424            let s ≝ set_arg_8 s ACC_A result in
    2525              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    2828            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    2929                                                   (get_arg_8 s false addr2) old_cy_flag in
    30             let cy_flag ≝ get_index … flags Z ? in
    31             let ac_flag ≝ get_index … flags one ? in
    32             let ov_flag ≝ get_index … flags two ? in
     30            let cy_flag ≝ get_index_v … flags Z ? in
     31            let ac_flag ≝ get_index_v … flags one ? in
     32            let ov_flag ≝ get_index_v … flags two ? in
    3333            let s ≝ set_arg_8 s ACC_A result in
    3434              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    3737            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
    3838                                                   (get_arg_8 s false addr2) old_cy_flag in
    39             let cy_flag ≝ get_index … flags Z ? in
    40             let ac_flag ≝ get_index … flags one ? in
    41             let ov_flag ≝ get_index … flags two ? in
     39            let cy_flag ≝ get_index_v … flags Z ? in
     40            let ac_flag ≝ get_index_v … flags one ? in
     41            let ov_flag ≝ get_index_v … flags two ? in
    4242            let s ≝ set_arg_8 s ACC_A result in
    4343              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    142142              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
    143143                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
    144                 let cy_flag ≝ get_index ? flags Z ? in
     144                let cy_flag ≝ get_index_v … flags Z ? in
    145145                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
    146146                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
     
    179179        | RL _ ⇒ (* DPM: always ACC_A *)
    180180            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    181             let new_acc ≝ rotate_left_bv ? one old_acc in
     181            let new_acc ≝ rotate_left … one old_acc in
    182182              set_8051_sfr s SFR_ACC_A new_acc
    183183        | RR _ ⇒ (* DPM: always ACC_A *)
    184184            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    185             let new_acc ≝ rotate_right_bv ? one old_acc in
     185            let new_acc ≝ rotate_right … one old_acc in
    186186              set_8051_sfr s SFR_ACC_A new_acc
    187187        | RLC _ ⇒ (* DPM: always ACC_A *)
    188188            let old_cy_flag ≝ get_cy_flag s in
    189189            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    190             let new_cy_flag ≝ get_index_bv ? old_acc Z ? in
    191             let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in
     190            let new_cy_flag ≝ get_index_v … old_acc Z ? in
     191            let new_acc ≝ shift_left … eight one old_acc old_cy_flag in
    192192            let s ≝ set_arg_1 s CARRY new_cy_flag in
    193193              set_8051_sfr s SFR_ACC_A new_acc
     
    195195            let old_cy_flag ≝ get_cy_flag s in
    196196            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    197             let new_cy_flag ≝ get_index_bv ? old_acc seven ? in
    198             let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in
     197            let new_cy_flag ≝ get_index_v … old_acc seven ? in
     198            let new_acc ≝ shift_right … eight one old_acc old_cy_flag in
    199199            let s ≝ set_arg_1 s CARRY new_cy_flag in
    200200              set_8051_sfr s SFR_ACC_A new_acc
     
    384384              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
    385385              let 〈nu, nl〉 ≝ split ? four four pc_bu in
    386               let bit ≝ get_index_bv ? nl Z ? in
     386              let bit ≝ get_index_v … nl Z ? in
    387387              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
    388388              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
  • Deliverables/D4.1/Matita/Status.ma

    r357 r362  
    191191    let sfr ≝ special_function_registers_8051 s in
    192192    let index ≝ sfr_8051_index i in
    193       get_index ?? sfr index ?.
    194     napply (sfr8051_index_nineteen i).
     193      get_index_v … sfr index ?.
     194    napply sfr8051_index_nineteen.
    195195nqed.
    196196
     
    200200    let sfr ≝ special_function_registers_8052 s in
    201201    let index ≝ sfr_8052_index i in
    202       get_index ?? sfr index ?.
    203     napply (sfr8052_index_five i).
     202      get_index_v … sfr index ?.
     203    napply sfr8052_index_five.
    204204nqed.
    205205
     
    383383  λs: Status.
    384384    let sfr ≝ special_function_registers_8051 s in
    385     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    386       get_index Bool eight psw Z ?.
     385    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     386      get_index_v Bool eight psw Z ?.
    387387    nnormalize.
    388388    napply (less_than_or_equal_monotone ? ?).
     
    395395  λs: Status.
    396396    let sfr ≝ special_function_registers_8051 s in
    397     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    398       get_index Bool eight psw (S Z) ?.
     397    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     398      get_index_v Bool eight psw (S Z) ?.
    399399    nnormalize.
    400400    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    407407  λs: Status.
    408408    let sfr ≝ special_function_registers_8051 s in
    409     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    410       get_index Bool eight psw two ?.
     409    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     410      get_index_v Bool eight psw two ?.
    411411    nnormalize.
    412412    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    419419  λs: Status.
    420420    let sfr ≝ special_function_registers_8051 s in
    421     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    422       get_index Bool eight psw three ?.
     421    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     422      get_index_v Bool eight psw three ?.
    423423    nnormalize.
    424424    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    431431  λs: Status.
    432432    let sfr ≝ special_function_registers_8051 s in
    433     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    434       get_index Bool eight psw four ?.
     433    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     434      get_index_v Bool eight psw four ?.
    435435    nnormalize.
    436436    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    443443  λs: Status.
    444444    let sfr ≝ special_function_registers_8051 s in
    445     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    446       get_index Bool eight psw five ?.
     445    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     446      get_index_v Bool eight psw five ?.
    447447    nnormalize.
    448448    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    455455  λs: Status.
    456456    let sfr ≝ special_function_registers_8051 s in
    457     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    458       get_index Bool eight psw six ?.
     457    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     458      get_index_v Bool eight psw six ?.
    459459    nnormalize.
    460460    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    467467  λs: Status.
    468468    let sfr ≝ special_function_registers_8051 s in
    469     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    470       get_index Bool eight psw seven ?.
     469    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     470      get_index_v Bool eight psw seven ?.
    471471    nnormalize.
    472472    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    482482  λov: Bit.
    483483    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
    484     let old_cy ≝ get_index … nu Z ? in
    485     let old_ac ≝ get_index … nu one ? in
    486     let old_fo ≝ get_index … nu two ? in
    487     let old_rs1 ≝ get_index … nu three ? in
    488     let old_rs0 ≝ get_index … nl Z ? in
    489     let old_ov ≝ get_index … nl one ? in
    490     let old_ud ≝ get_index … nl two ? in
    491     let old_p ≝ get_index … nl three ? in
     484    let old_cy ≝ get_index_v… nu Z ? in
     485    let old_ac ≝ get_index_v… nu one ? in
     486    let old_fo ≝ get_index_v… nu two ? in
     487    let old_rs1 ≝ get_index_v… nu three ? in
     488    let old_rs0 ≝ get_index_v… nl Z ? in
     489    let old_ov ≝ get_index_v… nl one ? in
     490    let old_ud ≝ get_index_v… nl two ? in
     491    let old_p ≝ get_index_v… nl three ? in
    492492    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
    493493    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
     
    655655  λs: Status.
    656656  λr: BitVector three.
    657     let b ≝ get_index_bv ? r Z ? in
    658     let c ≝ get_index_bv ? r one ? in
    659     let d ≝ get_index_bv ? r two ? in
     657    let b ≝ get_index_v … r Z ? in
     658    let c ≝ get_index_v … r one ? in
     659    let d ≝ get_index_v … r two ? in
    660660    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    661     let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_bv four un two ?) (get_index_bv four un three ?) in
     661    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_v … four un two ?) (get_index_v … four un three ?) in
    662662    let offset ≝
    663663      if conjunction (negation r1) (negation r0) then
     
    696696  λs: Status.
    697697    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    698     let m ≝ get_index_bv … nu Z ? in
    699     let r1 ≝ get_index_bv … nu one ? in
    700     let r2 ≝ get_index_bv … nu two ? in
    701     let r3 ≝ get_index_bv … nu three ? in
     698    let m ≝ get_index_v … nu Z ? in
     699    let r1 ≝ get_index_v … nu one ? in
     700    let r2 ≝ get_index_v … nu two ? in
     701    let r3 ≝ get_index_v … nu three ? in
    702702    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
    703703    let memory ≝
     
    719719  λv: Byte.
    720720    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    721     let bit_zero ≝ get_index … nu Z ? in
    722     let bit_one ≝ get_index … nu one ? in
    723     let bit_two ≝ get_index … nu two ? in
    724     let bit_three ≝ get_index … nu three ? in
     721    let bit_zero ≝ get_index_v… nu Z ? in
     722    let bit_one ≝ get_index_v… nu one ? in
     723    let bit_two ≝ get_index_v… nu two ? in
     724    let bit_three ≝ get_index_v… nu three ? in
    725725      if bit_zero then
    726726        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
     
    798798        λdirect: True.
    799799          let 〈 nu, nl 〉 ≝ split … four four d in
    800           let bit_one ≝ get_index_bv … nu one ? in
     800          let bit_one ≝ get_index_v … nu one ? in
    801801            match bit_one with
    802802              [ true ⇒
     
    810810          let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
    811811          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    812           let bit_one ≝ get_index_bv … bit_one_v Z ? in
     812          let bit_one ≝ get_index_v … bit_one_v Z ? in
    813813          match bit_one with
    814814            [ true ⇒
     
    837837        λdirect: True.
    838838          let 〈 nu, nl 〉 ≝ split … four four d in
    839           let bit_one ≝ get_index_bv … nu one ? in
     839          let bit_one ≝ get_index_v … nu one ? in
    840840          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    841841            match bit_one with
     
    849849          let register ≝ get_register s [[ false; false; i ]] in
    850850          let 〈 nu, nl 〉 ≝ split ? four four register in
    851           let bit_one ≝ get_index_bv ? nu one ? in
     851          let bit_one ≝ get_index_v … nu one ? in
    852852          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    853853          match bit_one with
     
    909909        λbit_addr: True.
    910910          let 〈 nu, nl 〉 ≝ split … four four b in
    911           let bit_one ≝ get_index_bv … nu one ? in
     911          let bit_one ≝ get_index_v … nu one ? in
    912912          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    913913            match bit_one with
     
    918918                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
    919919                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    920                   get_index_bv ? sfr m ?
     920                  get_index_v … sfr m ?
    921921              | false ⇒
    922922                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    923923                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    924924                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    925                   get_index_bv ? t (modulus address eight) ?
     925                  get_index_v … t (modulus address eight) ?
    926926              ]
    927927      | N_BIT_ADDR n ⇒
    928928        λn_bit_addr: True.
    929929          let 〈 nu, nl 〉 ≝ split … four four n in
    930           let bit_one ≝ get_index_bv … nu one ? in
     930          let bit_one ≝ get_index_v … nu one ? in
    931931          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    932932            match bit_one with
     
    937937                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
    938938                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    939                   negation (get_index_bv ? sfr m ?)
     939                  negation (get_index_v … sfr m ?)
    940940              | false ⇒
    941941                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    942942                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    943943                let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    944                   negation (get_index_bv ? trans (modulus address eight) ?)
     944                  negation (get_index_v … trans (modulus address eight) ?)
    945945              ]
    946946      | CARRY ⇒ λcarry: True. get_cy_flag s
     
    963963      [ BIT_ADDR b ⇒ λbit_addr: True.
    964964          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    965           let bit_one ≝ get_index_bv ? nu one ? in
     965          let bit_one ≝ get_index_v … nu one ? in
    966966          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    967967          match bit_one with
     
    985985        λcarry: True.
    986986          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    987           let bit_one ≝ get_index … nu one ? in
    988           let bit_two ≝ get_index … nu two ? in
    989           let bit_three ≝ get_index … nu three ? in
     987          let bit_one ≝ get_index_v… nu one ? in
     988          let bit_two ≝ get_index_v… nu two ? in
     989          let bit_three ≝ get_index_v… nu three ? in
    990990          let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
    991991            set_8051_sfr s SFR_PSW new_psw
  • Deliverables/D4.1/Matita/Vector.ma

    r357 r362  
    3030interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
    3131
     32notation "hvbox(l break !!! break n)"
     33  non associative with precedence 90
     34  for @{ 'get_index_v $l $n }.
     35
    3236(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3337(* Lookup.                                                                    *)
    3438(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3539
    36 nlet rec get_index (A: Type[0]) (n: Nat)
     40nlet rec get_index_v (A: Type[0]) (n: Nat)
    3741                   (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝
    3842  (match m with
     
    4549      (match v return λx.λ_. S o < x → A with
    4650        [ Empty ⇒ λprf: S o < Z. ?
    47         | Cons p hd tl ⇒ λprf: S o < S p. get_index A p tl o ?
     51        | Cons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
    4852        ])
    4953    ]) lt.
     
    5458nqed.
    5559
    56 nlet rec get_index_weak (A: Type[0]) (n: Nat)
     60nlet rec get_index_weak_v (A: Type[0]) (n: Nat)
    5761                   (v: Vector A n) (m: Nat) on m ≝
    5862  match m with
     
    6569      match v with
    6670        [ Empty ⇒ Nothing A
    67         | Cons p hd tl ⇒ get_index_weak A p tl o
    68         ]
    69     ].
    70    
    71 interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
     71        | Cons p hd tl ⇒ get_index_weak_v A p tl o
     72        ]
     73    ].
     74   
     75interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
    7276
    7377nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
Note: See TracChangeset for help on using the changeset viewer.