Lines Matching defs:subtypes
156 {facts : factdb, subtypes : vthm ovdiscrim};
193 PSUBTYPE_CONTEXT {facts = set_factdb, subtypes = empty_ovdiscrim};
197 val psubtype_context_subtypes = #subtypes o dest_psubtype_context;
198 fun psubtype_context_update_facts f (PSUBTYPE_CONTEXT {facts, subtypes}) =
199 PSUBTYPE_CONTEXT {facts = f facts, subtypes = subtypes};
200 fun psubtype_context_update_subtypes f (PSUBTYPE_CONTEXT {facts, subtypes}) =
201 PSUBTYPE_CONTEXT {facts = facts, subtypes = f subtypes};
236 add_string "#subtypes =",
238 pp_int (ovdiscrim_size (#subtypes c)),
408 val subtypes = SUBTYPE_CHECK false depth sc elt
409 val facts = factdb_add_vthms subtypes (subtype_context_facts sc)
438 {subtypes : subtype_context,
465 add_string "{subtypes =",
467 pp_subtype_context (#subtypes c),
507 {subtypes = new_subtype_context (),
514 val context_subtypes = #subtypes o dest_context;
521 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) =
522 CONTEXT {subtypes = f subtypes, forwards = forwards, rules = rules,
526 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) =
527 CONTEXT {subtypes = subtypes, forwards = f forwards, rules = rules,
531 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) =
532 CONTEXT {subtypes = subtypes, forwards = forwards, rules = f rules,
536 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) =
537 CONTEXT {subtypes = subtypes, forwards = forwards, rules = rules,
541 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) =
542 CONTEXT {subtypes = subtypes, forwards = forwards, rules = rules,