| /seL4-l4v-master/HOL4/examples/miller/subtypes/ |
| H A D | subtypeTools.sml | 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
408 val subtypes = SUBTYPE_CHECK false depth sc elt value
[all...] |
| H A D | subtypeScript.sml | 46 (* bool theory subtypes. *)
|
| /seL4-l4v-master/HOL4/src/quotient/src/ |
| H A D | quotient_optionScript.sml | 35 (* the corresponding functions/relations of the constituent subtypes *)
|
| H A D | quotient_sumScript.sml | 34 (* the corresponding functions/relations of the constituent subtypes *)
|
| H A D | quotient_pairScript.sml | 33 (* the corresponding functions/relations of the constituent subtypes *)
|
| H A D | quotient_listScript.sml | 37 (* the corresponding functions/relations of the constituent subtypes *)
|
| H A D | quotient_pred_setScript.sml | 38 (* the corresponding functions/relations of the constituent subtypes *)
|
| H A D | quotientScript.sml | 34 (* the corresponding functions/relations of the constituent subtypes *)
|
| H A D | quotient.sml | 3762 (* nstys holds all subtypes of the types in natys which contain a type
|
| /seL4-l4v-master/graph-refine/ |
| H A D | syntax.py | 313 def subtypes (self): member in class:Type
315 return structs[self.name].subtypes()
317 return [self] + self.el_typ.subtypes()
564 def subtypes (self): member in class:Struct
569 xs.extend(typ2.subtypes())
|
| /seL4-l4v-master/HOL4/examples/acl2/examples/ |
| H A D | miller-rabin.sml | 13 "../../miller/subtypes",
|
| /seL4-l4v-master/HOL4/src/quotient/choice/ |
| H A D | quotientScript.sml | 47 (* the corresponding functions/relations of the constituent subtypes *)
|
| /seL4-l4v-master/HOL4/src/res_quan/Manual/ |
| H A D | description.tex | 118 simulating subtypes and dependent types; the qualifying predicate $P$ can be
|
| /seL4-l4v-master/HOL4/examples/miller/groups/ |
| H A D | mult_groupScript.sml | 3 loadPath := ["../ho_prover","../subtypes","../RSA","../formalize"] @ !loadPath;
|
| H A D | extra_arithScript.sml | 3 loadPath := ["../ho_prover","../subtypes","../formalize"] @ !loadPath;
|
| /seL4-l4v-master/HOL4/examples/acl2/ml/ |
| H A D | encodeLib.sml | 1255 val subtypes = get_sub_types basetype t value
1260 subtypes
1972 val subtypes = sub_types t value
|
| /seL4-l4v-master/HOL4/Manual/Description/ |
| H A D | version2.tex | 79 simulating subtypes and dependent types; the qualifying predicate $p$ can be
272 Meeting and implements a method of simulating subtypes and dependent
|
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
| H A D | version2.tex | 79 simulating subtypes and dependent types; the qualifying predicate $p$ can be
272 Meeting and implements a method of simulating subtypes and dependent
|
| /seL4-l4v-master/HOL4/examples/set-theory/zfset/ |
| H A D | zfsetScript.sml | 1259 (* Restrictions of functions and binary operators to subtypes. *)
|
| /seL4-l4v-master/HOL4/src/quotient/Manual/ |
| H A D | quotient.tex | 667 equivalence relations for component subtypes, and return
677 Given equivalence theorems for the constituent subtypes, the
1530 constituent subtypes.
1594 % constituent subtypes of the aggregate type.
1602 given the quotient theorems for the subtypes which are the arguments to
1633 for the constituent subtypes that are arguments
1817 %that the constituent subtypes
|
| /seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
| H A D | CTT.tex | 569 versions of the other rules permit rewriting of subterms and subtypes.
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
| H A D | CTT.tex | 569 versions of the other rules permit rewriting of subterms and subtypes.
|
| /seL4-l4v-master/HOL4/Manual/Logic/ |
| H A D | semantics.tex | 1137 mechanism for introducing new types which are subtypes of existing
|