Changeset 746 for src/ASM/Util.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r715 r746  
    115115  λm, n: nat.
    116116    leb n m.
     117   
     118(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
     119let rec eq_nat (n: nat) (m: nat) on n: bool ≝
     120  match n with
     121  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
     122  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     123  ].
    117124
    118125(* dpm: conflicts with library definitions
Note: See TracChangeset for help on using the changeset viewer.