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/extranat.ma

    r961 r1515  
     1include "basics/types.ma".
    12include "arithmetics/nat.ma".
    23
     
    3637[ //
    3738| #m' #IH whd in ⊢ (??%?) > IH @refl
     39] qed.
     40
     41
     42let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝
     43match n return λn.Sum (n=m) (n≠m) with
     44[ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ]
     45| S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒
     46           match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ]
     47].
     48[ 1,2: % #E destruct
     49| >E @refl
     50| % #E destruct cases NE /2/
    3851] qed.
    3952
Note: See TracChangeset for help on using the changeset viewer.