Changeset 1515 for src/utilities/extranat.ma

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:

• src/utilities/extranat.ma (modified) (2 diffs)

src/utilities/extranat.ma

@@ +1 @@
+include "basics/types.ma".
 include "arithmetics/nat.ma".
 
@@ -36 +37 @@
 [ //
 | #m' #IH whd in ⊢ (??%?) > IH @refl
+] qed.
+
+
+let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝
+match n return λn.Sum (n=m) (n≠m) with
+[ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ]
+| S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒ 
+           match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ]
+].
+[ 1,2: % #E destruct
+| >E @refl
+| % #E destruct cases NE /2/
 ] qed.