package info (click to toggle)
acl2 8.5dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 991,452 kB
  • sloc: lisp: 15,567,759; javascript: 22,820; cpp: 13,929; ansic: 12,092; perl: 7,150; java: 4,405; xml: 3,884; makefile: 3,507; sh: 3,187; ruby: 2,633; ml: 763; python: 746; yacc: 723; awk: 295; csh: 186; php: 171; lex: 154; 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 big-proof-talks
d d rwxr-xr-x 129 gl-and-std
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,918 brr-free-variables-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-- 32,248 congruent-stobjs-log.txt
- - rw-r--r-- 1,156 constants-that-require-modifying-state.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,036 defabsstobj-example-4-input.lsp
- - rw-r--r-- 17,316 defabsstobj-example-4-log.txt
- - rw-r--r-- 11,800 defabsstobj-example-5.lisp
- - 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,121 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,860 memoize-invoke-input.lsp
- - rw-r--r-- 15,123 memoize-invoke-log.txt
- - rw-r--r-- 467 memoize-partial-book.acl2
- - rw-r--r-- 107 memoize-partial-book.lisp
- - rw-r--r-- 42,207 memoize-partial-input.lsp
- - rw-r--r-- 94,598 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-- 82,377 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-- 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