Changeset 1049 for src/utilities


Ignore:
Timestamp:
Jul 1, 2011, 5:45:46 PM (9 years ago)
Author:
mulligan
Message:

more stuff added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/HMap.ma

    r1048 r1049  
    55
    66include "arithmetics/nat.ma".
    7 include "basics/types.ma".
     7include "common/Order.ma".
    88
    99(* for eq_rect_Type0_r *)
     
    6464  | map_fork sz key elt l r ⇒ sz
    6565  ].
    66 
    67 inductive order: Type[0] ≝
    68   | order_lt: order
    69   | order_eq: order
    70   | order_gt: order.
    7166
    7267(* -------------------------------------------------------------------------- *)
Note: See TracChangeset for help on using the changeset viewer.