Changeset 746 for src/ASM/Util.ma

Timestamp:

Apr 8, 2011, 11:51:38 AM (9 years ago)

Author:

mulligan

Message:

Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.

File:

• src/ASM/Util.ma (modified) (1 diff)

src/ASM/Util.ma

@@ -115 +115 @@
   λm, n: nat.
     leb n m.
+    
+(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
+let rec eq_nat (n: nat) (m: nat) on n: bool ≝
+  match n with
+  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
+  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
+  ].
 
 (* dpm: conflicts with library definitions