| /seL4-l4v-master/HOL4/src/Boolify/src/ |
| H A D | PreListEncode.sig | 2 (* FILLING IN "BOOLIFY" ENTRIES IN THE TYPEBASE FOR TYPES BUILT BEFORE LISTS *)
|
| H A D | PreListEncode.sml | 2 (* FILLING IN "BOOLIFY" ENTRIES IN THE TYPEBASE FOR TYPES BUILT BEFORE LISTS *)
|
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Ordered.sig | 2 (* ORDERED TYPES *)
|
| H A D | Ordered.sml | 2 (* ORDERED TYPES *)
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Ordered.sig | 2 (* ORDERED TYPES *)
|
| H A D | Ordered.sml | 2 (* ORDERED TYPES *)
|
| /seL4-l4v-master/seL4/manual/tools/libsel4_tools/ |
| H A D | syscall_stub_gen.py | 83 TYPES = { variable
150 return "({0}) {1}".format(TYPES[self.size_bits], var_name)
152 return "({0}) ({1} >> {2})".format(TYPES[self.size_bits], var_name,
755 (param.name, TYPES[64], words[0] % source_words,
756 TYPES[64], words[1] % source_words))
|
| H A D | bitfield_gen.py | 71 TYPES = { variable
1749 {"type": TYPES[options.environment][self.base],
1771 'type': TYPES[options.environment][self.union_base],
1826 param_list = ["%s %s" % (TYPES[options.environment][self.base], field)
1843 f_value = "(%s)%s_%s" % (TYPES[options.environment][self.base], self.name, name)
1938 "type": TYPES[options.environment][ref.base],
2442 {"type": TYPES[options.environment][self.base],
2449 param_list = ["%s %s" % (TYPES[options.environment][self.base], field)
2547 "type": TYPES[options.environment][self.base],
|
| /seL4-l4v-master/seL4/libsel4/tools/ |
| H A D | syscall_stub_gen.py | 83 TYPES = { variable
150 return "({0}) {1}".format(TYPES[self.size_bits], var_name)
152 return "({0}) ({1} >> {2})".format(TYPES[self.size_bits], var_name,
755 (param.name, TYPES[64], words[0] % source_words,
756 TYPES[64], words[1] % source_words))
|
| H A D | bitfield_gen.py | 71 TYPES = { variable
1749 {"type": TYPES[options.environment][self.base],
1771 'type': TYPES[options.environment][self.union_base],
1826 param_list = ["%s %s" % (TYPES[options.environment][self.base], field)
1843 f_value = "(%s)%s_%s" % (TYPES[options.environment][self.base], self.name, name)
1938 "type": TYPES[options.environment][ref.base],
2442 {"type": TYPES[options.environment][self.base],
2449 param_list = ["%s %s" % (TYPES[options.environment][self.base], field)
2547 "type": TYPES[options.environment][self.base],
|
| /seL4-l4v-master/seL4/tools/ |
| H A D | bitfield_gen.py | 71 TYPES = { variable
1749 {"type": TYPES[options.environment][self.base],
1771 'type': TYPES[options.environment][self.union_base],
1826 param_list = ["%s %s" % (TYPES[options.environment][self.base], field)
1843 f_value = "(%s)%s_%s" % (TYPES[options.environment][self.base], self.name, name)
1938 "type": TYPES[options.environment][ref.base],
2442 {"type": TYPES[options.environment][self.base],
2449 param_list = ["%s %s" % (TYPES[options.environment][self.base], field)
2547 "type": TYPES[options.environment][self.base],
|
| /seL4-l4v-master/HOL4/src/quotient/examples/ |
| H A D | ext_finite_setScript.sml | 336 (* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *)
|
| H A D | msgScript.sml | 279 (* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *)
|
| H A D | finite_setScript.sml | 551 (* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *)
|
| /seL4-l4v-master/HOL4/src/quotient/examples/lambda/ |
| H A D | liftScript.sml | 981 (* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *)
|
| /seL4-l4v-master/HOL4/src/quotient/examples/sigma/ |
| H A D | liftScript.sml | 1482 (* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *)
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Prim_rec.sml | 1407 (* PROOF THAT CONSTRUCTORS OF RECURSIVE TYPES ARE ONE-TO-ONE *)
|
| /seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
| H A D | PKGS.sml | 2463 ("SET-INHIBITED-SUMMARY-TYPES" , "ACL2-USER" , "ACL2"),
4369 ("SET-INHIBITED-SUMMARY-TYPES" , "U" , "ACL2"),
6212 ("SET-INHIBITED-SUMMARY-TYPES" , "ACL2-ASG" , "ACL2"),
8061 ("SET-INHIBITED-SUMMARY-TYPES" , "ACL2-AGP" , "ACL2"),
9910 ("SET-INHIBITED-SUMMARY-TYPES" , "ACL2-CRG" , "ACL2"),
|
| H A D | axioms.ml | 9779 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
10332 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
10915 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
11493 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
11903 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
[all...] |
| /seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
| H A D | PKGS.sml | 2422 ("SET-INHIBITED-SUMMARY-TYPES" , "ACL2-USER" , "ACL2"),
4328 ("SET-INHIBITED-SUMMARY-TYPES" , "U" , "ACL2"),
6171 ("SET-INHIBITED-SUMMARY-TYPES" , "ACL2-ASG" , "ACL2"),
8020 ("SET-INHIBITED-SUMMARY-TYPES" , "ACL2-AGP" , "ACL2"),
9869 ("SET-INHIBITED-SUMMARY-TYPES" , "ACL2-CRG" , "ACL2"),
|
| /seL4-l4v-master/HOL4/src/quotient/src/ |
| H A D | quotient.sml | 4172 (* MAIN ENTRY POINT FOR SUBSET TYPES. *)
|
| /seL4-l4v-master/HOL4/src/quotient/Manual/ |
| H A D | quotient.tex | 5946 Proceedings of {\it TYPES 2002},
|
| /seL4-l4v-master/HOL4/examples/acl2/tests/round-trip/gold/ |
| H A D | axioms.sml | 9779 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
10332 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
10915 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
11493 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
11903 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "INHIBITED-SUMMARY-TYPES") (
[all...] |