File: unbound%40useless-runes.lsp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (111 lines) | stat: -rw-r--r-- 4,150 bytes parent folder | download | duplicates (6)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
(ADE::UNBOUND-IN-BODY)
(ADE::UNBOUND-IN-BODY-ATOM)
(ADE::UNBOUND-IN-BODY-LISTP
 (15 5 (:DEFINITION MEMBER-EQUAL))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (6 6 (:REWRITE ADE::UNBOUND-IN-BODY-ATOM))
 )
(ADE::ALL-UNBOUND-IN-BODY)
(ADE::ALL-UNBOUND-IN-BODY-ATOM)
(ADE::ALL-UNBOUND-IN-BODY-LISTP
 (45 10 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (40 10 (:REWRITE ADE::DISJOINT-ATOM))
 (20 20 (:DEFINITION ATOM))
 (10 10 (:TYPE-PRESCRIPTION ATOM))
 (6 6 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-CAR))
 )
(ADE::ALL-UNBOUND-IN-BODY-APPEND
 (331 100 (:REWRITE ADE::DISJOINT-ATOM))
 (77 77 (:TYPE-PRESCRIPTION ATOM))
 (40 10 (:DEFINITION BINARY-APPEND))
 (36 36 (:REWRITE DEFAULT-CAR))
 (25 25 (:REWRITE DEFAULT-CDR))
 (20 20 (:REWRITE APPEND-WHEN-NOT-CONSP))
 )
(ADE::ALL-UNBOUND-IN-BODY-CONS
 (460 115 (:REWRITE ADE::DISJOINT-ATOM))
 (246 63 (:DEFINITION MEMBER-EQUAL))
 (119 119 (:REWRITE DEFAULT-CDR))
 (115 115 (:TYPE-PRESCRIPTION ATOM))
 (114 114 (:REWRITE DEFAULT-CAR))
 )
(ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES
 (5 5 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::UNBOUND-IN-BODY-SE-OCC
 (648 8 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
 (381 24 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (328 48 (:REWRITE ADE::DISJOINT-ATOM))
 (275 25 (:DEFINITION PAIRLIS$))
 (261 186 (:REWRITE DEFAULT-CAR))
 (239 164 (:REWRITE DEFAULT-CDR))
 (224 16 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
 (208 48 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (192 8 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-DISJOINT))
 (152 8 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-SUBSET))
 (150 150 (:TYPE-PRESCRIPTION ADE::SE))
 (147 147 (:TYPE-PRESCRIPTION LEN))
 (136 136 (:TYPE-PRESCRIPTION STRIP-CARS))
 (129 129 (:TYPE-PRESCRIPTION PAIRLIS$))
 (128 128 (:TYPE-PRESCRIPTION ADE::DISJOINT))
 (128 16 (:DEFINITION TRUE-LISTP))
 (120 20 (:DEFINITION BINARY-APPEND))
 (120 8 (:DEFINITION SUBSETP-EQUAL))
 (105 21 (:DEFINITION LEN))
 (97 40 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (96 32 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (96 16 (:DEFINITION STRIP-CARS))
 (84 84 (:LINEAR LEN-WHEN-PREFIXP))
 (80 80 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (64 64 (:TYPE-PRESCRIPTION ADE::BVP))
 (57 11 (:DEFINITION MEMBER-EQUAL))
 (48 48 (:TYPE-PRESCRIPTION ATOM))
 (42 42 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (42 21 (:REWRITE DEFAULT-+-2))
 (40 40 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (24 24 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (21 21 (:REWRITE DEFAULT-+-1))
 (16 16 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (5 5 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (3 3 (:TYPE-PRESCRIPTION ADE::SE-OCC-INDUCT))
 )
(ADE::ALL-UNBOUND-IN-BODY-SE-OCC
 (1053 13 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
 (612 51 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (541 80 (:REWRITE ADE::DISJOINT-ATOM))
 (364 26 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
 (347 80 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (286 211 (:REWRITE DEFAULT-CAR))
 (281 206 (:REWRITE DEFAULT-CDR))
 (275 25 (:DEFINITION PAIRLIS$))
 (247 13 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-SUBSET))
 (231 231 (:TYPE-PRESCRIPTION LEN))
 (221 221 (:TYPE-PRESCRIPTION STRIP-CARS))
 (208 26 (:DEFINITION TRUE-LISTP))
 (195 13 (:DEFINITION SUBSETP-EQUAL))
 (165 165 (:TYPE-PRESCRIPTION PAIRLIS$))
 (165 33 (:DEFINITION LEN))
 (156 52 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (156 26 (:DEFINITION STRIP-CARS))
 (150 150 (:TYPE-PRESCRIPTION ADE::SE))
 (150 25 (:DEFINITION BINARY-APPEND))
 (132 132 (:LINEAR LEN-WHEN-PREFIXP))
 (130 130 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (113 50 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (104 104 (:TYPE-PRESCRIPTION ADE::BVP))
 (80 80 (:TYPE-PRESCRIPTION ATOM))
 (78 13 (:DEFINITION MEMBER-EQUAL))
 (66 66 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (66 33 (:REWRITE DEFAULT-+-2))
 (65 65 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (65 65 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (49 49 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (33 33 (:REWRITE DEFAULT-+-1))
 (26 26 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (11 11 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
 (3 3 (:TYPE-PRESCRIPTION ADE::SE-OCC-INDUCT))
 )