Searched refs:ASSOC (Results 1 - 25 of 34) sorted by relevance

12

/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/64/
H A Dcache.c52 #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 Dcache.c59 #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 Dcache.c59 #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 Dbasic_defaxioms.ml38 "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 Dbasic_defaxiomsScript.sml8 [("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 Dkpa-v2-9-3.ml44 ("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 Ddefaxioms.lisp.trans.ml592 (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 Dacl2_packageScript.sml155 ("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 Dhol_defaxiomsScript.sml506 [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 DcombinScript.sml342 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 DCSimp.sml21 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 Dtool.tex103 #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 Dtool.tex103 #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 Dproblem-set-1-answers.lisp2 '(&REST * + - / < <= > >= ACL2-COUNT AND ASSOC
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A DPKGS.sml219 ("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 Daxioms.ml741 (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 Dhol_defaxiomsScript.sml511 [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 DPKGS.sml178 ("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 DPKGS.lsp2 (("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 Dacl2_packageScript.sml155 ("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 Dhol_defaxiomsScript.sml510 [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 Daxioms.lisp258 (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 Daxioms.sml741 (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 DSERE.ml102 (``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 Dtest.sml145 val ASSOC_ADD = TAC_PROOF(([], --`ASSOC $+`--),

Completed in 601 milliseconds

12