Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (9 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

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

    r410 r465  
    1 include "Either.ma".
    21include "BitVector.ma".
    32include "String.ma".
     
    76| INDIRECT: Bit → addressing_mode
    87| EXT_INDIRECT: Bit → addressing_mode
    9 | REGISTER: BitVector (S (S (S Z))) → addressing_mode
     8| REGISTER: BitVector (S (S (S O))) → addressing_mode
    109| ACC_A: addressing_mode
    1110| ACC_B: addressing_mode
     
    9392
    9493
    95 nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : Bool ≝
    96  match l return λm.λ_:Vector addressing_mode_tag m.Bool with
     94nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
     95 match l return λm.λ_:Vector addressing_mode_tag m.bool with
    9796  [ VEmpty ⇒ false
    9897  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
     
    198197 | WithLabel: jump String → labelled_instruction.
    199198
    200 ndefinition preamble ≝ List (String × Nat).
    201 
    202 ndefinition assembly_program ≝ preamble × (List labelled_instruction).
     199ndefinition preamble ≝ list (String × nat).
     200
     201ndefinition assembly_program ≝ preamble × (list labelled_instruction).
Note: See TracChangeset for help on using the changeset viewer.