Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r1014 r1515  
    182182lemma get_8051_sfr_write_at_stack_pointer:
    183183 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
    184  #T #s #x #y whd in ⊢ (??%%) //
     184 #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl
    185185qed.
    186186
Note: See TracChangeset for help on using the changeset viewer.