1signature TypeNet = 2sig 3 4 (* signature names modelled on Binarymap's *) 5 type 'a typenet 6 type hol_type = Type.hol_type 7 8 val empty : 'a typenet 9 val insert : ('a typenet * hol_type * 'a) -> 'a typenet 10 val find : 'a typenet * hol_type -> 'a 11 val peek : 'a typenet * hol_type -> 'a option 12 val match : 'a typenet * hol_type -> (hol_type * 'a) list 13 14 val delete : 'a typenet * hol_type -> 'a typenet * 'a 15 val numItems : 'a typenet -> int 16 val listItems : 'a typenet -> (hol_type * 'a) list 17 val app : (hol_type * 'a -> unit) -> 'a typenet -> unit 18 val fold : (hol_type * 'a * 'b -> 'b) -> 'b -> 'a typenet -> 'b 19 20 val map : (hol_type * 'a -> 'b) -> 'a typenet -> 'b typenet 21 val transform : ('a -> 'b) -> 'a typenet -> 'b typenet 22 23end 24