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/utilities/extralib.ma

    r1350 r1515  
    389389definition mod ≝ λm,n. snd ?? (divide m n).
    390390
    391 lemma pred_minus: ∀n,m. pred n - m = pred (n-m).
     391lemma pred_minus: ∀n,m:Pos. pred n - m = pred (n-m).
    392392@pos_elim /3/;
    393393qed.
Note: See TracChangeset for help on using the changeset viewer.