package info (click to toggle)
acl2 8.6%2Bdfsg-3
  • links: PTS
  • area: main
  • in suites: sid
  • size: 1,138,276 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,978; makefile: 3,840; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17

Folder: demos

d .. (parent)
d d rwxr-xr-x 4,096 .sys
d d rwxr-xr-x 4,096 attach-stobj
d d rwxr-xr-x 4,096 big-proof-talks
d d rwxr-xr-x 4,096 event-data
d d rwxr-xr-x 153 gl-and-std
d d rwxr-xr-x 83 include-raw-examples
d d rwxr-xr-x 153 loop-primer
d d rwxr-xr-x 4,096 marktoberdorf-08
d d rwxr-xr-x 4,096 modeling
d d rwxr-xr-x 4,096 parallel
d d rwxr-xr-x 148 proofs
d d rwxr-xr-x 4,096 tutorial-problems
- - rw-r--r-- 2,906 Readme.lsp
- - rw-r--r-- 268 brr-free-variables-book.acl2
- - rw-r--r-- 113 brr-free-variables-book.lisp
- - rw-r--r-- 11,846 brr-free-variables-input.lsp
- - rw-r--r-- 36,579 brr-free-variables-log.txt
- - rw-r--r-- 204 brr-test-book.acl2
- - rw-r--r-- 192 brr-test-book.lisp
- - rw-r--r-- 10,253 brr-test-input.lsp
- - rw-r--r-- 32,020 brr-test-log.txt
- - rw-r--r-- 304 congruent-stobjs-book.acl2
- - rw-r--r-- 109 congruent-stobjs-book.lisp
- - rw-r--r-- 14,578 congruent-stobjs-input.lsp
- - rw-r--r-- 31,660 congruent-stobjs-log.txt
- - rw-r--r-- 1,156 constants-that-require-modifying-state.lisp
- - rw-r--r-- 20,103 defabsstobj-example-1-df.lisp
- - rw-r--r-- 19,201 defabsstobj-example-1.lisp
- - rw-r--r-- 12,016 defabsstobj-example-2.lisp
- - rw-r--r-- 13,419 defabsstobj-example-3.lisp
- - rw-r--r-- 505 defabsstobj-example-4-book.acl2
- - rw-r--r-- 119 defabsstobj-example-4-book.lisp
- - rw-r--r-- 5,028 defabsstobj-example-4-input.lsp
- - rw-r--r-- 16,987 defabsstobj-example-4-log.txt
- - rw-r--r-- 11,800 defabsstobj-example-5.lisp
- - rw-r--r-- 1,113 element-type.lisp
- - rw-r--r-- 382 floating-point-book.acl2
- - rw-r--r-- 1,201 floating-point-book.lisp
- - rw-r--r-- 69,945 floating-point-input.lsp
- - rw-r--r-- 170,521 floating-point-log.txt
- - rw-r--r-- 1,925 fp-raw.lsp
- - rw-r--r-- 63 fp.acl2
- - rw-r--r-- 6,302 fp.lisp
- - rw-r--r-- 257 geneqv-test-book.acl2
- - rw-r--r-- 139 geneqv-test-book.lisp
- - rw-r--r-- 7,906 geneqv-test-input.lsp
- - rw-r--r-- 51,614 geneqv-test-log.txt
- - rw-r--r-- 82 gl-and-use-example.acl2
- - rw-r--r-- 5,780 gl-and-use-example.lisp
- - rw-r--r-- 4,342 knuth-bendix-problem-1.lisp
- - rw-r--r-- 179 ld-history-book.acl2
- - rw-r--r-- 245 ld-history-book.lisp
- - rw-r--r-- 5,120 ld-history-input.lsp
- - rw-r--r-- 8,247 ld-history-log.txt
- - rw-r--r-- 35 list-equality-from-nth.acl2
- - rw-r--r-- 3,068 list-equality-from-nth.lisp
- - rw-r--r-- 2,196 list-theory.lisp
- - rw-r--r-- 2,602 measure-and-warrant.lisp
- - rw-r--r-- 408 memoize-invoke-book.acl2
- - rw-r--r-- 105 memoize-invoke-book.lisp
- - rw-r--r-- 2,911 memoize-invoke-input.lsp
- - rw-r--r-- 9,591 memoize-invoke-log.txt
- - rw-r--r-- 662 memoize-partial-book.acl2
- - rw-r--r-- 107 memoize-partial-book.lisp
- - rw-r--r-- 43,714 memoize-partial-input.lsp
- - rw-r--r-- 90,102 memoize-partial-log.txt
- - rw-r--r-- 20 meta-wf-guarantee-example.acl2
- - rw-r--r-- 22,102 meta-wf-guarantee-example.lisp
- - rw-r--r-- 188 mini-proveall-book.acl2
- - rw-r--r-- 282 mini-proveall-book.lisp
- - rw-r--r-- 328 mini-proveall-input.lsp
- - rw-r--r-- 81,641 mini-proveall-log.txt
- - rw-r--r-- 12,504 nth-update-nth-meta-extract.lisp
- - rw-r--r-- 509 partial-encapsulate-support-raw.lsp
- - rw-r--r-- 1,603 partial-encapsulate-support.lisp
- - rw-r--r-- 45 partial-encapsulate.acl2
- - rw-r--r-- 998 partial-encapsulate.lisp
- - rw-r--r-- 48,945 patterned-congruences.lisp
- - rw-r--r-- 2,288 ppr1-experiments-thm-1-ppr1.lisp
- - rw-r--r-- 18,255 ppr1-experiments.lisp
- - rw-r--r-- 940 r-and-i-answer-key-book.acl2
- - rw-r--r-- 113 r-and-i-answer-key-book.lisp
- - rw-r--r-- 125,118 r-and-i-answer-key-input.lsp
- - rw-r--r-- 1,793,497 r-and-i-answer-key-log.txt
- - rw-r--r-- 249 refinement-failure-test-book.acl2
- - rw-r--r-- 123 refinement-failure-test-book.lisp
- - rw-r--r-- 6,848 refinement-failure-test-input.lsp
- - rw-r--r-- 39,219 refinement-failure-test-log.txt
- - rw-r--r-- 91 register-invariant-risk-support.acl2
- - rw-r--r-- 950 register-invariant-risk-support.lisp
- - rw-r--r-- 30 register-invariant-risk.acl2
- - rw-r--r-- 1,830 register-invariant-risk.lisp
- - rw-r--r-- 5,885 rewrite-quoted-constant-examples-lemmas.lisp
- - rw-r--r-- 7,818 rewrite-quoted-constant-examples.lisp
- - rw-r--r-- 316 sort-by-car-pkg.lsp
- - rw-r--r-- 27 sort-by-car-support.acl2
- - rw-r--r-- 9,688 sort-by-car-support.lisp
- - rw-r--r-- 27 sort-by-car.acl2
- - rw-r--r-- 4,193 sort-by-car.lisp
- - rw-r--r-- 9,821 split-types-examples.lisp
- - rw-r--r-- 35 stobj-equality-from-fields.acl2
- - rw-r--r-- 2,795 stobj-equality-from-fields.lisp
- - rw-r--r-- 30,512 stobj-table-examples.lisp
- - rw-r--r-- 7,820 swap-stobj-fields.lisp
- - rw-r--r-- 7,729 toy-csort.lisp