/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/64/ |
H A D | cache.c | 52 #define ASSOC(s) ((((s) >> 3) & MASK(10)) + 1) macro 64 int assoc = ASSOC(lsize); 81 int assoc = ASSOC(lsize);
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv7-a/ |
H A D | cache.c | 59 #define ASSOC(s) ((((s) >> 3) & MASK(10)) + 1) macro 74 int assoc = ASSOC(s); 95 int assoc = ASSOC(s);
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/32/ |
H A D | cache.c | 59 #define ASSOC(s) ((((s) >> 3) & MASK(10)) + 1) macro 74 int assoc = ASSOC(s); 95 int assoc = ASSOC(s);
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | basic_defaxioms.ml | 38 "ACL2::ASSOC-EQ", 39 "ACL2::ASSOC-EQUAL", 40 "ACL2::ASSOC-EQ-EQUAL-ALISTP", 41 "ACL2::ASSOC-EQ-EQUAL", 63 "COMMON-LISP::ASSOC", 319 `(DEFUN ASSOC-EQ (X ALIST) 324 (ASSOC-EQ X (CDR ALIST)))))`, 327 `(DEFUN ASSOC-EQUAL (X ALIST) 332 (ASSOC-EQUAL X (CDR ALIST)))))`, 335 `(DEFUN ASSOC [all...] |
H A D | basic_defaxiomsScript.sml | 8 [("acl2_colon__colon_iff","ACL2::IFF"),("acl2_colon__colon_booleanp","ACL2::BOOLEANP"),("acl2_colon__colon_implies","ACL2::IMPLIES"),("common_lisp_colon__colon_not","COMMON-LISP::NOT"),("acl2_colon__colon_hide","ACL2::HIDE"),("common_lisp_colon__colon_eq","COMMON-LISP::EQ"),("acl2_colon__colon_true_listp","ACL2::TRUE-LISTP"),("acl2_colon__colon_list_macro","ACL2::LIST-MACRO"),("acl2_colon__colon_and_macro","ACL2::AND-MACRO"),("acl2_colon__colon_or_macro","ACL2::OR-MACRO"),("acl2_colon__colon_integer_abs","ACL2::INTEGER-ABS"),("acl2_colon__colon_xxxjoin","ACL2::XXXJOIN"),("acl2_colon__colon_len","ACL2::LEN"),("common_lisp_colon__colon_length","COMMON-LISP::LENGTH"),("acl2_colon__colon_acl2_count","ACL2::ACL2-COUNT"),("acl2_colon__colon_cond_clausesp","ACL2::COND-CLAUSESP"),("acl2_colon__colon_cond_macro","ACL2::COND-MACRO"),("acl2_colon__colon_eqlablep","ACL2::EQLABLEP"),("acl2_colon__colon_eqlable_listp","ACL2::EQLABLE-LISTP"),("common_lisp_colon__colon_atom","COMMON-LISP::ATOM"),("acl2_colon__colon_make_character_list","ACL2::MAKE-CHARACTER-LIST"),("acl2_colon__colon_eqlable_alistp","ACL2::EQLABLE-ALISTP"),("acl2_colon__colon_alistp","ACL2::ALISTP"),("common_lisp_colon__colon_acons","COMMON-LISP::ACONS"),("common_lisp_colon__colon_endp","COMMON-LISP::ENDP"),("acl2_colon__colon_must_be_equal","ACL2::MUST-BE-EQUAL"),("acl2_colon__colon_member_equal","ACL2::MEMBER-EQUAL"),("acl2_colon__colon_union_equal","ACL2::UNION-EQUAL"),("acl2_colon__colon_subsetp_equal","ACL2::SUBSETP-EQUAL"),("acl2_colon__colon_symbol_listp","ACL2::SYMBOL-LISTP"),("common_lisp_colon__colon_null","COMMON-LISP::NULL"),("acl2_colon__colon_member_eq","ACL2::MEMBER-EQ"),("acl2_colon__colon_subsetp_eq","ACL2::SUBSETP-EQ"),("acl2_colon__colon_symbol_alistp","ACL2::SYMBOL-ALISTP"),("acl2_colon__colon_assoc_eq","ACL2::ASSOC-EQ"),("acl2_colon__colon_assoc_equal","ACL2::ASSOC-EQUAL"),("acl2_colon__colon_assoc_eq_equal_alistp","ACL2::ASSOC-EQ-EQUAL-ALISTP"),("acl2_colon__colon_assoc_eq_equal","ACL2::ASSOC-EQ-EQUAL"),("acl2_colon__colon_no_duplicatesp_equal","ACL2::NO-DUPLICATESP-EQUAL"),("acl2_colon__colon_strip_cars","ACL2::STRIP-CARS"),("common_lisp_colon__colon_eql","COMMON-LISP::EQL"),("common_lisp_colon__colon__eq_","COMMON-LISP::="),("common_lisp_colon__colon__slash__eq_","COMMON-LISP::/="),("acl2_colon__colon_zp","ACL2::ZP"),("acl2_colon__colon_zip","ACL2::ZIP"),("common_lisp_colon__colon_nth","COMMON-LISP::NTH"),("common_lisp_colon__colon_char","COMMON-LISP::CHAR"),("acl2_colon__colon_proper_consp","ACL2::PROPER-CONSP"),("acl2_colon__colon_improper_consp","ACL2::IMPROPER-CONSP"),("common_lisp_colon__colon_conjugate","COMMON-LISP::CONJUGATE"),("acl2_colon__colon_prog2_dollar_","ACL2::PROG2$"),("acl2_colon__colon_time_dollar_","ACL2::TIME$"),("acl2_colon__colon_fix","ACL2::FIX"),("acl2_colon__colon_force","ACL2::FORCE"),("acl2_colon__colon_immediate_force_modep","ACL2::IMMEDIATE-FORCE-MODEP"),("acl2_colon__colon_case_split","ACL2::CASE-SPLIT"),("acl2_colon__colon_synp","ACL2::SYNP"),("common_lisp_colon__colon_member","COMMON-LISP::MEMBER"),("acl2_colon__colon_no_duplicatesp","ACL2::NO-DUPLICATESP"),("common_lisp_colon__colon_assoc","COMMON-LISP::ASSOC"),("acl2_colon__colon_r_eqlable_alistp","ACL2::R-EQLABLE-ALISTP"),("common_lisp_colon__colon_rassoc","COMMON-LISP::RASSOC"),("acl2_colon__colon_rassoc_equal","ACL2::RASSOC-EQUAL"),("acl2_colon__colon_r_symbol_alistp","ACL2::R-SYMBOL-ALISTP"),("acl2_colon__colon_rassoc_eq","ACL2::RASSOC-EQ")]; 601 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ") ( 613 "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" 619 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQUAL") ( 631 "ASSOC-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 638 "ASSOC [all...] |
H A D | kpa-v2-9-3.ml | 44 ("ALL-BOUNDP-PRESERVES-ASSOC", "ACL2-USER", "ACL2"), 68 ("ASSOC-ADD-PAIR", "ACL2-USER", "ACL2"), 69 ("ASSOC-EQ", "ACL2-USER", "ACL2"), 70 ("ASSOC-EQ-EQUAL", "ACL2-USER", "ACL2"), 71 ("ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"), 72 ("ASSOC-EQUAL", "ACL2-USER", "ACL2"), 73 ("ASSOC-KEYWORD", "ACL2-USER", "ACL2"), 74 ("ASSOC-STRING-EQUAL", "ACL2-USER", "ACL2"), 180 ("CONSP-ASSOC", "ACL2-USER", "ACL2"), 181 ("CONSP-ASSOC [all...] |
H A D | defaxioms.lisp.trans.ml | 592 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ") ( 604 "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" 610 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQUAL") ( 622 "ASSOC-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 629 "ASSOC-EQ-EQUAL-ALISTP") (mkpair (mkpair (mksym "ACL2" "X") (mksym 646 "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL-ALISTP") (mkpair ( 658 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") ( 677 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") ( 901 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ASSOC") ( 913 "ASSOC") (mkpai [all...] |
H A D | acl2_packageScript.sml | 155 ("ALL-BOUNDP-PRESERVES-ASSOC", "ACL2-USER", "ACL2"), 179 ("ASSOC-ADD-PAIR", "ACL2-USER", "ACL2"), 180 ("ASSOC-EQ", "ACL2-USER", "ACL2"), 181 ("ASSOC-EQ-EQUAL", "ACL2-USER", "ACL2"), 182 ("ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"), 183 ("ASSOC-EQUAL", "ACL2-USER", "ACL2"), 184 ("ASSOC-KEYWORD", "ACL2-USER", "ACL2"), 185 ("ASSOC-STRING-EQUAL", "ACL2-USER", "ACL2"), 291 ("CONSP-ASSOC", "ACL2-USER", "ACL2"), 292 ("CONSP-ASSOC [all...] |
H A D | hol_defaxiomsScript.sml | 506 [oracles: DEFUN ACL2::ASSOC-EQ, DISK_THM] [axioms: ] [] 513 [oracles: DEFUN ACL2::ASSOC-EQUAL, DISK_THM] [axioms: ] [] 520 [oracles: DEFUN ACL2::ASSOC-EQ-EQUAL-ALISTP, DISK_THM] [axioms: ] [] 529 [oracles: DEFUN ACL2::ASSOC-EQ-EQUAL, DISK_THM] [axioms: ] [] 693 [oracles: DEFUN COMMON-LISP::ASSOC, DISK_THM] [axioms: ] [] 700 acl2_defn "COMMON-LISP::ASSOC" 1344 [oracles: DEFUN ACL2::ASSOC-STRING-EQUAL, DISK_THM] [axioms: ] [] 2546 [oracles: DEFUN ACL2::ASSOC-KEYWORD, DISK_THM] [axioms: ] [] 4052 [oracles: DEFUN ACL2::PUT-ASSOC-EQ, DISK_THM] [axioms: ] [] 4061 [oracles: DEFUN ACL2::PUT-ASSOC [all...] |
/seL4-l4v-master/HOL4/src/combin/ |
H A D | combinScript.sml | 342 ASSOC (f:'a->'a->'a) <=> (!x y z. f x (f y z) = f (f x y) z) 368 ASSOC f /\ RIGHT_ID f e /\ LEFT_ID f e 375 val ASSOC_CONJ = store_thm ("ASSOC_CONJ", ``ASSOC $/\``, 385 ``ASSOC $\/``, 389 ``!f: 'a->'a->'a. FCOMM f f = ASSOC f``,
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | CSimp.sml | 21 fun find_atom ASSOC COMM dthis is_other t = let 22 val find_atom = find_atom ASSOC COMM dthis is_other 25 if is_this (lhand t) then REWR_CONV (GSYM ASSOC) t
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | tool.tex | 103 #let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3";; 104 ASSOC = |- (t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3 152 #REWR_CONV ASSOC "(A /\ B) /\ C";; 155 #REWR_CONV ASSOC "A /\ (B /\ C)";; 256 \ml{REWR\_CONV\ ASSOC} 295 #REWR_CONV ASSOC ex1;; 298 #TOP_DEPTH_CONV (REWR_CONV ASSOC) ex1;; 360 # TOP_DEPTH_CONV(REWR_CONV ASSOC) THENC 414 let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3" 430 TOP_DEPTH_CONV(REWR_CONV ASSOC) THEN [all...] |
/seL4-l4v-master/HOL4/Manual/Tutorial/ |
H A D | tool.tex | 103 #let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3";; 104 ASSOC = |- (t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3 152 #REWR_CONV ASSOC "(A /\ B) /\ C";; 155 #REWR_CONV ASSOC "A /\ (B /\ C)";; 256 \ml{REWR\_CONV\ ASSOC} 295 #REWR_CONV ASSOC ex1;; 298 #TOP_DEPTH_CONV (REWR_CONV ASSOC) ex1;; 360 # TOP_DEPTH_CONV(REWR_CONV ASSOC) THENC 414 let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3" 430 TOP_DEPTH_CONV(REWR_CONV ASSOC) THEN [all...] |
/seL4-l4v-master/HOL4/examples/acl2/tests/gold/ |
H A D | problem-set-1-answers.lisp | 2 '(&REST * + - / < <= > >= ACL2-COUNT AND ASSOC
|
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | PKGS.sml | 219 ("ASSOC" , "ACL2" , "COMMON-LISP"), 222 ("ASSOC-IF" , "ACL2" , "COMMON-LISP"), 225 ("ASSOC-IF-NOT" , "ACL2" , "COMMON-LISP"), 1146 ("ALL-BOUNDP-PRESERVES-ASSOC" , "ACL2-USER" , "ACL2"), 1201 ("ASSOC" , "ACL2-USER" , "COMMON-LISP"), 1202 ("ASSOC-ADD-PAIR" , "ACL2-USER" , "ACL2"), 1203 ("ASSOC-EQ" , "ACL2-USER" , "ACL2"), 1204 ("ASSOC-EQ-EQUAL" , "ACL2-USER" , "ACL2"), 1205 ("ASSOC-EQ-EQUAL-ALISTP" , "ACL2-USER" , "ACL2"), 1206 ("ASSOC [all...] |
H A D | axioms.ml | 741 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ") ( 753 "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" 759 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQUAL") ( 771 "ASSOC-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 778 "ASSOC-EQ-EQUAL-ALISTP") (mkpair (mkpair (mksym "ACL2" "X") (mksym 795 "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL-ALISTP") (mkpair ( 807 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") ( 826 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") ( 1665 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ASSOC") ( 1677 "ASSOC") (mkpai [all...] |
H A D | hol_defaxiomsScript.sml | 511 [oracles: DEFUN ACL2::ASSOC-EQ, DISK_THM] [axioms: ] [] 518 [oracles: DEFUN ACL2::ASSOC-EQUAL, DISK_THM] [axioms: ] [] 525 [oracles: DEFUN ACL2::ASSOC-EQ-EQUAL-ALISTP, DISK_THM] [axioms: ] [] 534 [oracles: DEFUN ACL2::ASSOC-EQ-EQUAL, DISK_THM] [axioms: ] [] 698 [oracles: DEFUN COMMON-LISP::ASSOC, DISK_THM] [axioms: ] [] 705 acl2_defn "COMMON-LISP::ASSOC" 1349 [oracles: DEFUN ACL2::ASSOC-STRING-EQUAL, DISK_THM] [axioms: ] [] 2588 [oracles: DEFUN ACL2::ASSOC-KEYWORD, DISK_THM] [axioms: ] [] 4094 [oracles: DEFUN ACL2::PUT-ASSOC-EQ, DISK_THM] [axioms: ] [] 4103 [oracles: DEFUN ACL2::PUT-ASSOC [all...] |
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
H A D | PKGS.sml | 178 ("ASSOC" , "ACL2" , "COMMON-LISP"), 181 ("ASSOC-IF" , "ACL2" , "COMMON-LISP"), 184 ("ASSOC-IF-NOT" , "ACL2" , "COMMON-LISP"), 1105 ("ALL-BOUNDP-PRESERVES-ASSOC" , "ACL2-USER" , "ACL2"), 1160 ("ASSOC" , "ACL2-USER" , "COMMON-LISP"), 1161 ("ASSOC-ADD-PAIR" , "ACL2-USER" , "ACL2"), 1162 ("ASSOC-EQ" , "ACL2-USER" , "ACL2"), 1163 ("ASSOC-EQ-EQUAL" , "ACL2-USER" , "ACL2"), 1164 ("ASSOC-EQ-EQUAL-ALISTP" , "ACL2-USER" , "ACL2"), 1165 ("ASSOC [all...] |
H A D | PKGS.lsp | 2 (("ACL2-CRG" & &ALLOW-OTHER-KEYS &AUX &BODY &ENVIRONMENT &KEY &OPTIONAL &REST &WHOLE * ** *** *ACL2-EXPORTS* *BREAK-ON-SIGNALS* *COMMON-LISP-SPECIALS-AND-CONSTANTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE* *COMPILE-FILE-PATHNAME* *COMPILE-FILE-TRUENAME* *COMPILE-PRINT* *COMPILE-VERBOSE* *DEBUG-IO* *DEBUGGER-HOOK* *DEFAULT-PATHNAME-DEFAULTS* *ERROR-OUTPUT* *FEATURES* *GENSYM-COUNTER* *LOAD-PATHNAME* *LOAD-PRINT* *LOAD-TRUENAME* *LOAD-VERBOSE* *MACROEXPAND-HOOK* *MAIN-LISP-PACKAGE-NAME* *MODULES* *PACKAGE* *PRINT-ARRAY* *PRINT-BASE* *PRINT-CASE* *PRINT-CIRCLE* *PRINT-ESCAPE* *PRINT-GENSYM* *PRINT-LENGTH* *PRINT-LEVEL* *PRINT-LINES* *PRINT-MISER-WIDTH* *PRINT-PPRINT-DISPATCH* *PRINT-PRETTY* *PRINT-RADIX* *PRINT-READABLY* *PRINT-RIGHT-MARGIN* *QUERY-IO* *RANDOM-STATE* *READ-BASE* *READ-DEFAULT-FLOAT-FORMAT* *READ-EVAL* *READ-SUPPRESS* *READTABLE* *STANDARD-CHARS* *STANDARD-CI* *STANDARD-CO* *STANDARD-INPUT* *STANDARD-OI* *STANDARD-OUTPUT* *TERMINAL-IO* *TRACE-OUTPUT* + ++ +++ - / // /// /= 1+ 1- 32-BIT-INTEGER-LISTP 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP 32-BIT-INTEGER-STACK 32-BIT-INTEGER-STACK-LENGTH 32-BIT-INTEGER-STACK-LENGTH1 32-BIT-INTEGERP 32-BIT-INTEGERP-FORWARD-TO-INTEGERP < <-ON-OTHERS <= = > >= ?-FN @ ABORT ABORT! ABS ACCUMULATED-PERSISTENCE ACL2-COUNT ACL2-INPUT-CHANNEL-PACKAGE ACL2-NUMBERP ACL2-ORACLE ACL2-OUTPUT-CHANNEL-PACKAGE ACL2-PACKAGE ACONS ACOS ACOSH ACTIVE-RUNEP ADD-BINOP ADD-DEFAULT-HINTS ADD-DEFAULT-HINTS! ADD-INVISIBLE-FNS ADD-MACRO-ALIAS ADD-METHOD ADD-NTH-ALIAS ADD-PAIR ADD-PAIR-PRESERVES-ALL-BOUNDP ADD-TIMERS ADD-TO-SET-EQ ADD-TO-SET-EQL ADD-TO-SET-EQUAL ADJOIN ADJUST-ARRAY ADJUSTABLE-ARRAY-P ALISTP ALISTP-FORWARD-TO-TRUE-LISTP ALL-BOUNDP ALL-BOUNDP-PRESERVES-ASSOC ALL-VARS ALL-VARS1 ALL-VARS1-LST ALLOCATE-INSTANCE ALPHA-CHAR-P ALPHA-CHAR-P-FORWARD-TO-CHARACTERP ALPHANUMERICP AND AND-MACRO APPEND APPLY APROPOS APROPOS-LIST AREF AREF-32-BIT-INTEGER-STACK AREF-T-STACK AREF1 AREF2 ARGS ARITHMETIC-ERROR ARITHMETIC-ERROR-OPERANDS ARITHMETIC-ERROR-OPERATION ARRAY ARRAY-DIMENSION ARRAY-DIMENSION-LIMIT ARRAY-DIMENSIONS ARRAY-DISPLACEMENT ARRAY-ELEMENT-TYPE ARRAY-HAS-FILL-POINTER-P ARRAY-IN-BOUNDS-P ARRAY-RANK ARRAY-RANK-LIMIT ARRAY-ROW-MAJOR-INDEX ARRAY-TOTAL-SIZE ARRAY-TOTAL-SIZE-LIMIT ARRAY1P ARRAY1P-CONS ARRAY1P-FORWARD ARRAY1P-LINEAR ARRAY2P ARRAY2P-CONS ARRAY2P-FORWARD ARRAY2P-LINEAR ARRAYP ASET-32-BIT-INTEGER-STACK ASET-T-STACK ASET1 ASET2 ASH ASIN ASINH ASSERT ASSERT$ ASSIGN ASSOC ASSOC-ADD-PAIR ASSOC-EQ ASSOC-EQ-EQUAL ASSOC-EQ-EQUAL-ALISTP ASSOC-EQUAL ASSOC-IF ASSOC-IF-NOT ASSOC [all...] |
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | acl2_packageScript.sml | 155 ("ALL-BOUNDP-PRESERVES-ASSOC", "ACL2-USER", "ACL2"), 179 ("ASSOC-ADD-PAIR", "ACL2-USER", "ACL2"), 180 ("ASSOC-EQ", "ACL2-USER", "ACL2"), 181 ("ASSOC-EQ-EQUAL", "ACL2-USER", "ACL2"), 182 ("ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"), 183 ("ASSOC-EQUAL", "ACL2-USER", "ACL2"), 184 ("ASSOC-KEYWORD", "ACL2-USER", "ACL2"), 185 ("ASSOC-STRING-EQUAL", "ACL2-USER", "ACL2"), 291 ("CONSP-ASSOC", "ACL2-USER", "ACL2"), 292 ("CONSP-ASSOC [all...] |
H A D | hol_defaxiomsScript.sml | 510 [oracles: DEFUN ACL2::ASSOC-EQ, DISK_THM] [axioms: ] [] 517 [oracles: DEFUN ACL2::ASSOC-EQUAL, DISK_THM] [axioms: ] [] 524 [oracles: DEFUN ACL2::ASSOC-EQ-EQUAL-ALISTP, DISK_THM] [axioms: ] [] 533 [oracles: DEFUN ACL2::ASSOC-EQ-EQUAL, DISK_THM] [axioms: ] [] 697 [oracles: DEFUN COMMON-LISP::ASSOC, DISK_THM] [axioms: ] [] 704 acl2_defn "COMMON-LISP::ASSOC" 1348 [oracles: DEFUN ACL2::ASSOC-STRING-EQUAL, DISK_THM] [axioms: ] [] 2550 [oracles: DEFUN ACL2::ASSOC-KEYWORD, DISK_THM] [axioms: ] [] 4056 [oracles: DEFUN ACL2::PUT-ASSOC-EQ, DISK_THM] [axioms: ] [] 4065 [oracles: DEFUN ACL2::PUT-ASSOC [all...] |
/seL4-l4v-master/HOL4/examples/acl2/tests/round-trip/gold/ |
H A D | axioms.lisp | 258 (DEFUN ASSOC-EQ (X ALIST) 263 (ASSOC-EQ X (CDR ALIST))))) 265 (DEFUN ASSOC-EQUAL (X ALIST) 270 (ASSOC-EQUAL X (CDR ALIST))))) 272 (DEFUN ASSOC-EQ-EQUAL-ALISTP (X) 278 (ASSOC-EQ-EQUAL-ALISTP (CDR X)) 283 (DEFUN ASSOC-EQ-EQUAL (X Y ALIST) 290 (ASSOC-EQ-EQUAL X Y (CDR ALIST))))) 559 (DEFUN ASSOC (X ALIST) function 564 (ASSOC [all...] |
H A D | axioms.sml | 741 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ") ( 753 "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" 759 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQUAL") ( 771 "ASSOC-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 778 "ASSOC-EQ-EQUAL-ALISTP") (mkpair (mkpair (mksym "ACL2" "X") (mksym 795 "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL-ALISTP") (mkpair ( 807 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") ( 826 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") ( 1665 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ASSOC") ( 1677 "ASSOC") (mkpai [all...] |
/seL4-l4v-master/HOL4/examples/PSL/experimental-semantics/ |
H A D | SERE.ml | 102 (``ASSOC $*``, 558 (``!l x y. ASSOC f ==> (FOLDL f (f x y) l = f x (FOLDL f y l))``,
|
/seL4-l4v-master/HOL4/src/list/examples/ |
H A D | test.sml | 145 val ASSOC_ADD = TAC_PROOF(([], --`ASSOC $+`--),
|