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/binary/positive.ma

    r1330 r1515  
    656656definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ].
    657657
    658 interpretation "natural minus" 'minus x y = (minus x y).
     658interpretation "positive minus" 'minus x y = (minus x y).
    659659
    660660lemma partialminus_S: ∀n,m:Pos.
     
    942942  ].
    943943
    944 theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.
     944theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Type[0].
    945945(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
    946946#n elim n;
     
    11591159
    11601160definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
     1161
     1162
     1163
     1164definition max : Pos → Pos → Pos ≝
     1165λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
Note: See TracChangeset for help on using the changeset viewer.