Lines Matching refs:ASSOC
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)
564 (ASSOC X (CDR ALIST)))))
694 (ASSOC X
727 (ASSOC X
817 (ASSOC CH
948 (DEFUN ASSOC-STRING-EQUAL (STR ALIST)
953 (ASSOC-STRING-EQUAL STR (CDR ALIST)))))
1188 CDAADR ASSERT BOOLE-ORC1 CDAAR ASSOC
1189 BOOLE-ORC2 CDADAR ASSOC-IF BOOLE-SET
1190 CDADDR ASSOC-IF-NOT BOOLE-XOR CDADR
1880 (IF (IF (ASSOC-EQ 'DEFUN-NX DEFS)
1881 (ASSOC-EQ 'DEFUN-NX DEFS)
1882 (ASSOC-EQ 'DEFUND-NX DEFS))
2570 (ASSOC TREE ALIST)
2596 (DEFTHM PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP
2598 (ASSOC-EQ-EQUAL-ALISTP X)))
2717 (IF (ASSOC-EQ (CAR (CDR (CAR WORLD-ALIST)))
2849 (DEFUN ASSOC-KEYWORD (KEY L)
2853 L (ASSOC-KEYWORD KEY (CDR (CDR L))))))
2855 (DEFTHM KEYWORD-VALUE-LISTP-ASSOC-KEYWORD
2857 (KEYWORD-VALUE-LISTP (ASSOC-KEYWORD KEY L))))
2859 (DEFTHM CONSP-ASSOC-EQ
2861 (IF (CONSP (ASSOC-EQ NAME L))
2862 (CONSP (ASSOC-EQ NAME L))
2863 (EQUAL (ASSOC-EQ NAME L) 'NIL))))
2893 (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2895 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
2899 (CDR (ASSOC-EQ ':HEADER L))
2913 (KEYWORD-VALUE-LISTP (CDR (ASSOC-EQ ':HEADER L)))
2915 (TRUE-LISTP (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2916 (CDR (ASSOC-EQ ':HEADER L))))))
2919 (LENGTH (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2920 (CDR (ASSOC-EQ ':HEADER L))))))
2924 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2925 (CDR (ASSOC-EQ ':HEADER L)))))))
2927 (INTEGERP (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
2928 (CDR (ASSOC-EQ ':HEADER L))))))
2931 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2932 (CDR (ASSOC-EQ ':HEADER L)))))))
2934 (< (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2935 (CDR (ASSOC-EQ ':HEADER L))))))
2936 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
2937 (CDR (ASSOC-EQ ':HEADER L))))))
2940 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
2941 (CDR (ASSOC-EQ ':HEADER L)))))))
2944 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2945 (CDR (ASSOC-EQ ':HEADER L)))))))
2962 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2963 (CDR (ASSOC-EQ ':HEADER L)))))))
2964 (IF (< (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
2965 (CDR (ASSOC-EQ ':HEADER L))))))
2966 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
2967 (CDR (ASSOC-EQ ':HEADER L))))))
2969 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
2970 (CDR (ASSOC-EQ ':HEADER L)))))))
3064 (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3066 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
3070 (CDR (ASSOC-EQ ':HEADER L))
3084 (KEYWORD-VALUE-LISTP (CDR (ASSOC-EQ ':HEADER L)))
3086 (TRUE-LISTP (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3087 (CDR (ASSOC-EQ ':HEADER L))))))
3090 (LENGTH (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3091 (CDR (ASSOC-EQ ':HEADER L))))))
3095 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3096 (CDR (ASSOC-EQ ':HEADER L)))))))
3100 (CDR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3101 (CDR (ASSOC-EQ ':HEADER L))))))))
3103 (INTEGERP (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
3104 (CDR (ASSOC-EQ ':HEADER L))))))
3107 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3108 (CDR (ASSOC-EQ ':HEADER L)))))))
3113 (CDR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3114 (CDR (ASSOC-EQ ':HEADER L))))))))
3118 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3119 (CDR (ASSOC-EQ ':HEADER L))))))
3122 (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3123 (CDR (ASSOC-EQ ':HEADER L))))))))
3124 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
3125 (CDR (ASSOC-EQ ':HEADER L))))))
3129 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
3130 (CDR (ASSOC-EQ ':HEADER L)))))))
3133 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3134 (CDR (ASSOC-EQ ':HEADER L))))))
3137 (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3138 (CDR (ASSOC-EQ ':HEADER L))))))))
3158 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3159 (CDR (ASSOC-EQ ':HEADER L)))))))
3162 (CAR (CDR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3163 (CDR (ASSOC-EQ ':HEADER L))))))))
3167 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3168 (CDR (ASSOC-EQ ':HEADER L))))))
3169 (CAR (CDR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3170 (CDR (ASSOC-EQ ':HEADER L))))))))
3171 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
3172 (CDR (ASSOC-EQ ':HEADER L))))))
3174 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
3175 (CDR (ASSOC-EQ ':HEADER L)))))))
3180 (DEFUN HEADER (NAME L) (PROG2$ NAME (ASSOC-EQ ':HEADER L)))
3183 (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3187 (CAR (CDR (ASSOC-KEYWORD ':MAXIMUM-LENGTH
3191 (CAR (CDR (ASSOC-KEYWORD ':DEFAULT
3194 (DEFTHM CONSP-ASSOC
3196 (IF (CONSP (ASSOC NAME L))
3197 (CONSP (ASSOC NAME L))
3198 (EQUAL (ASSOC NAME L) 'NIL))))
3204 (ASSOC N L)
3220 (ASSOC I L)
3235 (ASSOC-KEYWORD ':ORDER (CDR HEADER))))
3275 (CAR (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3276 (CDR (ASSOC-EQ ':HEADER L)))))))
3513 (IF (ASSOC (CAR (CAR ALIST1)) ALIST2)
3908 SUBLIS ACONS ASSOC RASSOC NTH SUBSEQ
3915 ASSOC-EQ ASSOC-EQUAL MEMBER-EQ
4104 (PLIST-WORLDP (CDR (ASSOC 'CURRENT-ACL2-WORLD
4110 (CDR (ASSOC 'CURRENT-ACL2-WORLD
4113 (TIMER-ALISTP (CDR (ASSOC 'TIMER-ALIST (GLOBAL-TABLE X))))
4118 (CDR (ASSOC 'CURRENT-ACL2-WORLD
4286 SUBLIS ACONS ASSOC RASSOC NTH SUBSEQ
4293 ASSOC-EQ ASSOC-EQUAL MEMBER-EQ
4482 (PLIST-WORLDP (CDR (ASSOC 'CURRENT-ACL2-WORLD (NTH '2 X))))
4487 (CDR (ASSOC 'CURRENT-ACL2-WORLD
4490 (TIMER-ALISTP (CDR (ASSOC 'TIMER-ALIST (NTH '2 X))))
4495 (CDR (ASSOC 'CURRENT-ACL2-WORLD
4662 SUBLIS ACONS ASSOC RASSOC NTH SUBSEQ
4669 ASSOC-EQ ASSOC-EQUAL MEMBER-EQ
4895 (IF (ASSOC X (GLOBAL-TABLE STATE-STATE))
4914 (CDR (ASSOC X (GLOBAL-TABLE STATE-STATE))))
4936 (ASSOC-EQ
5045 SUBLIS ACONS ASSOC RASSOC NTH SUBSEQ
5052 ASSOC-EQ ASSOC-EQUAL MEMBER-EQ
5238 (ASSOC-EQ
5347 SUBLIS ACONS ASSOC RASSOC NTH SUBSEQ
5354 ASSOC-EQ ASSOC-EQUAL MEMBER-EQ
5540 (ASSOC-EQ
5828 (IF (SYMBOLP KEY) (ASSOC-EQ KEY L) 'NIL)
5948 (IF (ASSOC-EQ (CAR (CAR ALIST1)) ALIST2)
6056 (DEFTHM TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ
6058 (TRUE-LISTP (ASSOC-EQ KEY L))))
6060 (DEFTHM TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P
6062 (TRUE-LISTP (CAR (CDR (ASSOC-EQ KEY ALIST))))))
6070 (ASSOC-EQ CHANNEL
6080 (ASSOC-EQ CHANNEL
6211 (EQ (CDR (ASSOC-EQ 'PRINT-CASE
6218 (CDR (ASSOC-EQ 'PRINT-BASE
6223 (CDR (ASSOC-EQ CHANNEL
6234 (CDR (ASSOC-EQ CHANNEL
6245 (CDR (ASSOC-EQ CHANNEL
6291 (ASSOC-EQUAL (CONS FILE-NAME
6336 (CDR (CAR (CDR (ASSOC-EQ CHANNEL
6461 (ASSOC-EQ CHANNEL
6478 (CDR (ASSOC-EQ CHANNEL
6484 (CDR (ASSOC-EQ CHANNEL
6497 (CDR (ASSOC-EQ CHANNEL
6516 (CDR (ASSOC-EQ CHANNEL
6674 (DEFTHM ALL-BOUNDP-PRESERVES-ASSOC
6678 (IF (SYMBOLP X) (ASSOC-EQ X TBL1) 'NIL)
6682 (ASSOC X TBL2)))
6861 (DEFUN PUT-ASSOC-EQ (NAME VAL ALIST)
6867 (PUT-ASSOC-EQ NAME VAL (CDR ALIST))))))
6869 (DEFUN PUT-ASSOC-EQL (NAME VAL ALIST)
6875 (PUT-ASSOC-EQL NAME VAL (CDR ALIST))))))
6877 (DEFUN PUT-ASSOC-EQUAL (NAME VAL ALIST)
6883 (PUT-ASSOC-EQUAL NAME VAL (CDR ALIST))))))
6887 (PUT-ASSOC-EQ NAME
6892 (CDR (ASSOC-EQ NAME (GET-GLOBAL 'TIMER-ALIST STATE))))
6954 (DEFTHM ASSOC-ADD-PAIR
6958 (EQUAL (ASSOC SYM1 (ADD-PAIR SYM2 VAL ALIST))
6961 (ASSOC SYM1 ALIST)))))
7092 (CAR (CDR (ASSOC-EQUAL (GET-GLOBAL 'CURRENT-PACKAGE STATE)
7147 (DEFTHM TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQUAL
7149 (TRUE-LISTP (ASSOC-EQUAL KEY L))))
7301 (IF (CDR (ASSOC-EQ ':VERIFY-GUARDS-EAGERNESS
7304 (CDR (ASSOC-EQ ':VERIFY-GUARDS-EAGERNESS
7310 (CDR (ASSOC-EQ ':COMPILE-FNS
7329 (IF (CDR (ASSOC-EQ ':MEASURE-FUNCTION
7332 (CDR (ASSOC-EQ ':MEASURE-FUNCTION
7338 (IF (CDR (ASSOC-EQ ':WELL-FOUNDED-RELATION
7341 (CDR (ASSOC-EQ ':WELL-FOUNDED-RELATION
7350 (CDR (ASSOC-EQ ':DEFUN-MODE
7379 (DEFUN DELETE-ASSOC-EQ (KEY ALIST)
7385 (DELETE-ASSOC-EQ KEY (CDR ALIST))))))
7387 (DEFUN DELETE-ASSOC-EQUAL (KEY ALIST)
7393 (DELETE-ASSOC-EQUAL KEY (CDR ALIST))))))
7400 (IF (CDR (ASSOC-EQ ':BACKCHAIN-LIMIT
7403 (CDR (ASSOC-EQ ':BACKCHAIN-LIMIT
7414 (IF (CDR (ASSOC-EQ ':DEFAULT-BACKCHAIN-LIMIT
7417 (CDR (ASSOC-EQ ':DEFAULT-BACKCHAIN-LIMIT
7424 (IF (CDR (ASSOC-EQ ':REWRITE-STACK-LIMIT
7427 (CDR (ASSOC-EQ ':REWRITE-STACK-LIMIT
7433 (CDR (ASSOC-EQ ':CASE-SPLIT-LIMITATIONS
7440 (CDR (ASSOC-EQ ':MATCH-FREE-DEFAULT
7450 (CONS (CDR (ASSOC-EQ ':MATCH-FREE-OVERRIDE-NUME
7454 (ASSOC-EQ ':MATCH-FREE-OVERRIDE
7461 (ASSOC-EQ ':NON-LINEARP
7470 (CDR (ASSOC-EQ 'T