Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 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/joint/TranslateUtils.ma

    r1352 r1515  
    2424    cases (fresh_regs pars0 globals def m) normalize nodelta
    2525    #def' #regs #EQ change in EQ with (|regs| = m) <EQ
    26     change with
    27     (|let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ?| = ?)
    28     cases (fresh … (joint_if_runiverse … def')) normalize // ]
     26    @refl
     27 ]
    2928qed.
    3029
Note: See TracChangeset for help on using the changeset viewer.