Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (9 years ago)
Author:
sacerdot
Message:
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File:
1 edited

Legend:

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

    r256 r260  
    11include "Universes.ma".
    2 include "Equality.ma".
     2include "Plogic/equality.ma".
    33include "Either.ma".
    44include "BitVector.ma".
     
    3636nlet rec is_a (d:all_types) (A:addressing_mode) on d ≝
    3737  match d with
    38    [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ True | _ ⇒ False ]
    39    | data ⇒ match A with [ DATA _ ⇒ True | _ ⇒ False ]
    40    | rel ⇒ match A with [ RELATIVE _ ⇒ True | _ ⇒ False ]
    41    | acc ⇒ match A with [ ACCUMULATORA ⇒ True | _ ⇒ False ]
    42    | direct ⇒ match A with [ DIRECT _ ⇒ True | _ ⇒ False ]
    43    | indirect ⇒ match A with [ INDIRECT _ ⇒ True | _ ⇒ False ]].
     38   [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ true | _ ⇒ false ]
     39   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
     40   | rel ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
     41   | acc ⇒ match A with [ ACCUMULATORA ⇒ true | _ ⇒ false ]
     42   | direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
     43   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]].
    4444
    4545interpretation "Bool" 'or a b = (inclusive_disjunction a b).
     
    5959 { subaddressing_modeel:> addressing_mode;
    6060   subaddressing_modein:
    61     match is_in ? l subaddressing_modeel with [ True ⇒ (? : Prop) | False ⇒ (? : Prop) ]
     61    match is_in ? l subaddressing_modeel with [ true ⇒ (? : Prop) | false ⇒ (? : Prop) ]
    6262 }.
    6363##[ napply True | napply False ]
     
    8787
    8888ndefinition xxx: Jump Nat.
    89  napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [True] [True] [True]) ?) (Z: Nat)).
     89 napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [true] [true] [true]) ?) (Z: Nat)).
    9090 napply I;
    9191nqed.
     
    110110interpretation "Sigma" 'sigma T = (Sigma ? T).
    111111
    112 ndefinition true: Bool ≝ True.
    113 ndefinition false: Bool ≝ False.
    114112naxiom daemon: False.
    115113
Note: See TracChangeset for help on using the changeset viewer.