Searched defs:map_entry (Results 1 - 4 of 4) sorted by relevance

/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DAList.sig18 val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c) value
H A DAList.sml51 fun map_entry eq key f = function
H A DTable.sml41 val map_entry: key -> ('a -> 'a) (*exception SAME*) -> 'a table -> 'a table value
293 fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x); function
H A DGraph.sml135 fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab); function

Completed in 29 milliseconds