[acl2/acl2] 098ac7: [C$] Update some doc.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 098ac78c7641e927fb49f857b45b625b344ce314
https://github.com/acl2/acl2/commit/098ac78c7641e927fb49f857b45b625b344ce314
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-23 (Mon, 23 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Update some doc.


Commit: 53f5565a30fbffb24db76911536b177daaed72d8
https://github.com/acl2/acl2/commit/53f5565a30fbffb24db76911536b177daaed72d8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-23 (Mon, 23 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp

Log Message:
-----------
[C$] Fix XDOC topic name.


Commit: 88df41a160f7c1dfb88d09a264ef461602caf732
https://github.com/acl2/acl2/commit/88df41a160f7c1dfb88d09a264ef461602caf732
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-23 (Mon, 23 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Extend ASTs with `#define` directives.


Commit: be50c99abcf6e9162be36ebc5de4d7c5807012d9
https://github.com/acl2/acl2/commit/be50c99abcf6e9162be36ebc5de4d7c5807012d9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-23 (Mon, 23 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Extend ASTs with `#undef` directives.


Commit: 77e85700a3145b8bc09657b0f80dd43ea0cef913
https://github.com/acl2/acl2/commit/77e85700a3145b8bc09657b0f80dd43ea0cef913
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-23 (Mon, 23 Mar 2026)

Changed paths:
M GNUmakefile
M acl2-check.lisp
M acl2-fns.lisp
M acl2-init.lisp
M acl2.lisp
M akcl-acl2-trace.lisp
M allegro-acl2-trace.lisp
M apply-constraints.lisp
M apply-prim.lisp
M apply-raw.lisp
M apply.lisp
M axioms.lisp
M basis-a.lisp
M basis-b.lisp
M bdd.lisp
M books/Makefile-generic
M books/Makefile-psubdirs
M books/Makefile-subdirs
M books/build/universal-dependency.certdep
M books/centaur/esim/tests/.sys/com...@useless-runes.lsp
M books/centaur/esim/tutorial/.sys/in...@useless-runes.lsp
M books/centaur/gl/.sys/gl-generic-...@useless-runes.lsp
M books/centaur/gl/.sys/gl-generic-...@useless-runes.lsp
M books/centaur/gl/.sys/gl-gener...@useless-runes.lsp
M books/centaur/gl/.sys/gl-t...@useless-runes.lsp
M books/centaur/gl/.sys/g...@useless-runes.lsp
M books/centaur/gl/.sys/glcp-rewr...@useless-runes.lsp
M books/centaur/gl/.sys/rewrite...@useless-runes.lsp
M books/centaur/gl/.sys/run-gi...@useless-runes.lsp
M books/centaur/glmc/.sys/glmc-gene...@useless-runes.lsp
M books/centaur/glmc/.sys/gl...@useless-runes.lsp
M books/centaur/meta/.sys/bindi...@useless-runes.lsp
M books/centaur/meta/.sys/congr...@useless-runes.lsp
M books/centaur/meta/.sys/equiv...@useless-runes.lsp
A books/centaur/meta/.sys/fixed-e...@useless-runes.lsp
A books/centaur/meta/.sys/fnsy...@useless-runes.lsp
M books/centaur/meta/.sys/lambda-...@useless-runes.lsp
M books/centaur/meta/.sys/let...@useless-runes.lsp
M books/centaur/meta/.sys/parse-...@useless-runes.lsp
M books/centaur/meta/.sys/pseudo-re...@useless-runes.lsp
A books/centaur/meta/.sys/pseudo-ter...@useless-runes.lsp
A books/centaur/meta/.sys/subst...@useless-runes.lsp
M books/centaur/meta/.sys/su...@useless-runes.lsp
M books/centaur/meta/.sys/subst...@useless-runes.lsp
M books/centaur/meta/.sys/term...@useless-runes.lsp
M books/centaur/meta/.sys/unify-...@useless-runes.lsp
M books/centaur/meta/.sys/urew...@useless-runes.lsp
M books/centaur/meta/.sys/variab...@useless-runes.lsp
M books/centaur/misc/.sys/bound-r...@useless-runes.lsp
M books/centaur/misc/.sys/conte...@useless-runes.lsp
M books/centaur/misc/.sys/defa...@useless-runes.lsp
M books/centaur/misc/.sys/evaluator-m...@useless-runes.lsp
M books/centaur/misc/.sys/interp-func...@useless-runes.lsp
M books/centaur/sv/svex/.sys/evals-eq...@useless-runes.lsp
M books/centaur/sv/svex/.sys/svex-env-...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-ge...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-sto...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-stobj-...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-...@useless-runes.lsp
M books/centaur/svl/.sys/svex-s...@useless-runes.lsp
M books/centaur/svl/.sys/svl-f...@useless-runes.lsp
M books/centaur/svl/.sys/type...@useless-runes.lsp
M books/centaur/svl/meta/.sys/4vec-r...@useless-runes.lsp
M books/centaur/svl/meta/.sys/bits...@useless-runes.lsp
M books/centaur/svl/meta/.sys/svex-eval...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/ba...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/integerp...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/simplify-bi...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/svex-reduc...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/desig...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/desig...@useless-runes.lsp
M books/clause-processors/.sys/ev-th...@useless-runes.lsp
M books/clause-processors/.sys/indu...@useless-runes.lsp
M books/clause-processors/.sys/just-...@useless-runes.lsp
M books/clause-processors/.sys/meta-ext...@useless-runes.lsp
M books/clause-processors/.sys/replace-e...@useless-runes.lsp
M books/clause-processors/.sys/witne...@useless-runes.lsp
M books/demos/gl-and-std/.sys/defaggregat...@useless-runes.lsp
M books/demos/gl-and-std/.sys/defaggrega...@useless-runes.lsp
M books/demos/gl-and-std/.sys/defprod-...@useless-runes.lsp
M books/doc/.sys/public...@useless-runes.lsp
M books/doc/relnotes.lisp
M books/emacs/acl2-doc-open-url.el
M books/emacs/acl2-doc.el
M books/emacs/emacs-acl2.el
M books/emacs/html-to-xdoc.el
M books/emacs/monitor.el
M books/hints/.sys/basic...@useless-runes.lsp
M books/kestrel/.sys/top...@useless-runes.lsp
M books/kestrel/.sys/t...@useless-runes.lsp
A books/kestrel/abstract-domains/.sys/t...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/arith...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/co...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/ex...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/i...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/min-max...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/noninterval-...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/portc...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/subint...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/t...@useless-runes.lsp
A books/kestrel/abstract-domains/many-valued-logics/.sys/3...@useless-runes.lsp
A books/kestrel/abstract-domains/many-valued-logics/.sys/t...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/aref1...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/evaluati...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/evalu...@useless-runes.lsp
A books/kestrel/air/.sys/portc...@useless-runes.lsp
A books/kestrel/air/.sys/t...@useless-runes.lsp
A books/kestrel/air/model-0/.sys/library-e...@useless-runes.lsp
A books/kestrel/air/model-0/.sys/portc...@useless-runes.lsp
A books/kestrel/air/model-0/.sys/t...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/corre...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/exa...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/field-e...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/fi...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/pfcs-con...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/pfcs-l...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/tra...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/abstrac...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/dynamic-...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/exa...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/input-outpu...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/alists-light/.sys/acons-...@useless-runes.lsp
A books/kestrel/apt/.sys/simplify-conj...@useless-runes.lsp
A books/kestrel/apt/.sys/simplify-c...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/l...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/m...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/m...@useless-runes.lsp
R books/kestrel/arm/.sys/ar...@useless-runes.lsp
M books/kestrel/arm/.sys/dec...@useless-runes.lsp
A books/kestrel/arm/.sys/def-...@useless-runes.lsp
A books/kestrel/arm/.sys/d...@useless-runes.lsp
A books/kestrel/arm/.sys/enco...@useless-runes.lsp
A books/kestrel/arm/.sys/instru...@useless-runes.lsp
A books/kestrel/arm/.sys/memo...@useless-runes.lsp
M books/kestrel/arm/.sys/mem...@useless-runes.lsp
M books/kestrel/arm/.sys/pseud...@useless-runes.lsp
A books/kestrel/arm/.sys/ru...@useless-runes.lsp
M books/kestrel/arm/.sys/st...@useless-runes.lsp
A books/kestrel/arm/.sys/st...@useless-runes.lsp
A books/kestrel/arm/.sys/t...@useless-runes.lsp
A books/kestrel/arm/tests/.sys/sim...@useless-runes.lsp
M books/kestrel/auto-termination/.sys/defunt...@useless-runes.lsp
M books/kestrel/axe/.sys/add-and-nor...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bitxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bitxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/add-t...@useless-runes.lsp
M books/kestrel/axe/.sys/alist-suitab...@useless-runes.lsp
M books/kestrel/axe/.sys/assumpti...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-bind-free-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-clause...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax-fun...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntaxp-e...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-tr...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-...@useless-runes.lsp
M books/kestrel/axe/.sys/bitops...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-d...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-array-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-intr...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-list-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/cars-decre...@useless-runes.lsp
M books/kestrel/axe/.sys/cars-incre...@useless-runes.lsp
M books/kestrel/axe/.sys/concretize-w...@useless-runes.lsp
M books/kestrel/axe/.sys/conjoin-te...@useless-runes.lsp
M books/kestrel/axe/.sys/conjunctions-a...@useless-runes.lsp
M books/kestrel/axe/.sys/consec...@useless-runes.lsp
M books/kestrel/axe/.sys/cont...@useless-runes.lsp
M books/kestrel/axe/.sys/cont...@useless-runes.lsp
M books/kestrel/axe/.sys/convert-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/count-b...@useless-runes.lsp
M books/kestrel/axe/.sys/crunc...@useless-runes.lsp
M books/kestrel/axe/.sys/crunc...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-arr...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-parent-ar...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pare...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pare...@useless-runes.lsp
A books/kestrel/axe/.sys/dag-pr...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-si...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-siz...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-to-ter...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-t...@useless-runes.lsp
M books/kestrel/axe/.sys/dag...@useless-runes.lsp
M books/kestrel/axe/.sys/dag...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/darg-...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/def-simpli...@useless-runes.lsp
M books/kestrel/axe/.sys/def-sim...@useless-runes.lsp
M books/kestrel/axe/.sys/defthm-a...@useless-runes.lsp
M books/kestrel/axe/.sys/defth...@useless-runes.lsp
M books/kestrel/axe/.sys/depth...@useless-runes.lsp
M books/kestrel/axe/.sys/el...@useless-runes.lsp
M books/kestrel/axe/.sys/equality-assu...@useless-runes.lsp
M books/kestrel/axe/.sys/equality-a...@useless-runes.lsp
M books/kestrel/axe/.sys/equivalen...@useless-runes.lsp
M books/kestrel/axe/.sys/equival...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluat...@useless-runes.lsp
A books/kestrel/axe/.sys/evaluato...@useless-runes.lsp
M books/kestrel/axe/.sys/eval...@useless-runes.lsp
M books/kestrel/axe/.sys/extract-...@useless-runes.lsp
M books/kestrel/axe/.sys/find-probable...@useless-runes.lsp
M books/kestrel/axe/.sys/find-probable...@useless-runes.lsp
M books/kestrel/axe/.sys/find-prob...@useless-runes.lsp
M books/kestrel/axe/.sys/fixup-...@useless-runes.lsp
M books/kestrel/axe/.sys/get-args...@useless-runes.lsp
M books/kestrel/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/.sys/hit-c...@useless-runes.lsp
M books/kestrel/axe/.sys/identical...@useless-runes.lsp
M books/kestrel/axe/.sys/instantiat...@useless-runes.lsp
M books/kestrel/axe/.sys/instant...@useless-runes.lsp
M books/kestrel/axe/.sys/keep-node...@useless-runes.lsp
M books/kestrel/axe/.sys/known-b...@useless-runes.lsp
M books/kestrel/axe/.sys/leaves-of-normal...@useless-runes.lsp
M books/kestrel/axe/.sys/leaves-of-norma...@useless-runes.lsp
M books/kestrel/axe/.sys/lifter...@useless-runes.lsp
M books/kestrel/axe/.sys/make-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-bind-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ax...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ax...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-syntaxp...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-synt...@useless-runes.lsp
M books/kestrel/axe/.sys/make-conju...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag-co...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag-va...@useless-runes.lsp
M books/kestrel/axe/.sys/make-equ...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ev...@useless-runes.lsp
M books/kestrel/axe/.sys/make-impli...@useless-runes.lsp
M books/kestrel/axe/.sys/make-node-rep...@useless-runes.lsp
M books/kestrel/axe/.sys/make-prov...@useless-runes.lsp
M books/kestrel/axe/.sys/make-rewri...@useless-runes.lsp
M books/kestrel/axe/.sys/make-subcor-var-an...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-in...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-in...@useless-runes.lsp
M books/kestrel/axe/.sys/match-hyp-with-node...@useless-runes.lsp
M books/kestrel/axe/.sys/memoi...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-dag-in...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-greater-tha...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-less-than...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-nodes-i...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-sort-le...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-tree-into...@useless-runes.lsp
M books/kestrel/axe/.sys/node...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replacement-...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/normali...@useless-runes.lsp
M books/kestrel/axe/.sys/numeri...@useless-runes.lsp
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/.sys/prover...@useless-runes.lsp
M books/kestrel/axe/.sys/prover...@useless-runes.lsp
M books/kestrel/axe/.sys/prover-st...@useless-runes.lsp
M books/kestrel/axe/.sys/pro...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag...@useless-runes.lsp
M books/kestrel/axe/.sys/prune...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-with-c...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-wit...@useless-runes.lsp
M books/kestrel/axe/.sys/pure-da...@useless-runes.lsp
M books/kestrel/axe/.sys/pure...@useless-runes.lsp
M books/kestrel/axe/.sys/rationa...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuild-...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuild...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuil...@useless-runes.lsp
M books/kestrel/axe/.sys/refine-as...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assu...@useless-runes.lsp
M books/kestrel/axe/.sys/remove-duplicates...@useless-runes.lsp
M books/kestrel/axe/.sys/remov...@useless-runes.lsp
M books/kestrel/axe/.sys/renamin...@useless-runes.lsp
M books/kestrel/axe/.sys/renumber...@useless-runes.lsp
M books/kestrel/axe/.sys/replac...@useless-runes.lsp
M books/kestrel/axe/.sys/replace-usin...@useless-runes.lsp
M books/kestrel/axe/.sys/replace-...@useless-runes.lsp
M books/kestrel/axe/.sys/result...@useless-runes.lsp
M books/kestrel/axe/.sys/result-ar...@useless-runes.lsp
M books/kestrel/axe/.sys/result...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter-...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter-...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/speci...@useless-runes.lsp
M books/kestrel/axe/.sys/spli...@useless-runes.lsp
M books/kestrel/axe/.sys/stored...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-clause...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-count...@useless-runes.lsp
M books/kestrel/axe/.sys/sublis-var-a...@useless-runes.lsp
M books/kestrel/axe/.sys/sublis-va...@useless-runes.lsp
M books/kestrel/axe/.sys/substitu...@useless-runes.lsp
M books/kestrel/axe/.sys/substit...@useless-runes.lsp
M books/kestrel/axe/.sys/supporti...@useless-runes.lsp
M books/kestrel/axe/.sys/support...@useless-runes.lsp
M books/kestrel/axe/.sys/sweep-and-m...@useless-runes.lsp
M books/kestrel/axe/.sys/tactic...@useless-runes.lsp
M books/kestrel/axe/.sys/term-eq...@useless-runes.lsp
M books/kestrel/axe/.sys/test-...@useless-runes.lsp
M books/kestrel/axe/.sys/translate-...@useless-runes.lsp
M books/kestrel/axe/.sys/translat...@useless-runes.lsp
M books/kestrel/axe/.sys/trim-intro...@useless-runes.lsp
M books/kestrel/axe/.sys/type-in...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-and-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-and...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-ter...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-tre...@useless-runes.lsp
M books/kestrel/axe/.sys/unroll-s...@useless-runes.lsp
M books/kestrel/axe/.sys/wf-...@useless-runes.lsp
M books/kestrel/axe/.sys/worklis...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/assum...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/axe-...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/d...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/eval...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/portc...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/rewr...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/rule-...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/run-unti...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/sup...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/syntaxp-...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/t...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/unro...@useless-runes.lsp
A books/kestrel/axe/arm/examples/add/.sys/add-with...@useless-runes.lsp
A books/kestrel/axe/arm/examples/add/.sys/a...@useless-runes.lsp
M books/kestrel/axe/examples/.sys/aes-blas...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-bind-free...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntaxp-...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/evalua...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/jvm-rul...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/jvm-ru...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lif...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/nice-output...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/symbolic-exe...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/tes...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unrolle...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-evalu...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-pro...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-syntaxp-e...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift-r1...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/verif...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/clear-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/eval...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/lifter...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/read-an...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/read-over-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/regi...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/rewr...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/run-unti...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/sup...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/syntax-f...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/syntaxp-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/write-over-...@useless-runes.lsp
M books/kestrel/axe/risc-v/examples/add/.sys/add-n...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/bind-free-e...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/evalua...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/lifter-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/loop-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/prove-eq...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/syntaxp-ev...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tester-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tes...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/unroller-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/unro...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/with-suppo...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/x86-...@useless-runes.lsp
M books/kestrel/axe/x86/examples/switch/.sys/sup...@useless-runes.lsp
M books/kestrel/bibtex/.sys/xdoc-ge...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/all-unsign...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/append...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/array-o...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/array-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-con...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-ar...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-read...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arr...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-list-read...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvchop...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvcho...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvnot...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvxor-li...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvxor...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/byte-f...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bytes-t...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/getbi...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/list-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/logex...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-bvp...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-packbv-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-pack...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-reve...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/negated-e...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-little-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pack...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unpackb...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unpa...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unsigned-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/width-of-...@useless-runes.lsp
M books/kestrel/bv/.sys/ad...@useless-runes.lsp
M books/kestrel/bv/.sys/a...@useless-runes.lsp
M books/kestrel/bv/.sys/b...@useless-runes.lsp
M books/kestrel/bv/.sys/bit-t...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bi...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bool-...@useless-runes.lsp
A books/kestrel/bv/.sys/bvan...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bva...@useless-runes.lsp
M books/kestrel/bv/.sys/bvcat...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvc...@useless-runes.lsp
M books/kestrel/bv/.sys/bvc...@useless-runes.lsp
M books/kestrel/bv/.sys/bvdiv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvequa...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
A books/kestrel/bv/.sys/bvmin...@useless-runes.lsp
M books/kestrel/bv/.sys/bvm...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvmult...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvp...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvsx-...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
A books/kestrel/bv/.sys/bvumin...@useless-runes.lsp
M books/kestrel/bv/.sys/bvum...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/convert-t...@useless-runes.lsp
M books/kestrel/bv/.sys/de...@useless-runes.lsp
M books/kestrel/bv/.sys/getbit...@useless-runes.lsp
M books/kestrel/bv/.sys/get...@useless-runes.lsp
M books/kestrel/bv/.sys/idi...@useless-runes.lsp
M books/kestrel/bv/.sys/if-becomes...@useless-runes.lsp
M books/kestrel/bv/.sys/in...@useless-runes.lsp
M books/kestrel/bv/.sys/leftrota...@useless-runes.lsp
M books/kestrel/bv/.sys/leftro...@useless-runes.lsp
M books/kestrel/bv/.sys/leftr...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/ones-co...@useless-runes.lsp
M books/kestrel/bv/.sys/overflow-an...@useless-runes.lsp
M books/kestrel/bv/.sys/put...@useless-runes.lsp
M books/kestrel/bv/.sys/right...@useless-runes.lsp
M books/kestrel/bv/.sys/rot...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/ru...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvdiv...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvdivdo...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvlt...@useless-runes.lsp
M books/kestrel/bv/.sys/sb...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvmo...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvrem...@useless-runes.lsp
M books/kestrel/bv/.sys/sbv...@useless-runes.lsp
M books/kestrel/bv/.sys/singl...@useless-runes.lsp
M books/kestrel/bv/.sys/slice...@useless-runes.lsp
M books/kestrel/bv/.sys/sli...@useless-runes.lsp
M books/kestrel/bv/.sys/sl...@useless-runes.lsp
M books/kestrel/bv/.sys/s...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-elim...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-elim-r...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-int...@useless-runes.lsp
M books/kestrel/bv/.sys/unsigned-byte-...@useless-runes.lsp
M books/kestrel/c/atc/.sys/gener...@useless-runes.lsp
M books/kestrel/c/atc/.sys/pretty-...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-expr...@useless-runes.lsp
R books/kestrel/c/atc/symbolic-execution-rules/.sys/exec...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/li...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/object-de...@useless-runes.lsp
M books/kestrel/c/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/c/language/.sys/computati...@useless-runes.lsp
A books/kestrel/c/language/.sys/decimal-0-...@useless-runes.lsp
M books/kestrel/c/language/.sys/frame-and-s...@useless-runes.lsp
M books/kestrel/c/language/.sys/function-e...@useless-runes.lsp
M books/kestrel/c/language/.sys/keyw...@useless-runes.lsp
A books/kestrel/c/language/.sys/punct...@useless-runes.lsp
M books/kestrel/c/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/c/language/.sys/tag-envi...@useless-runes.lsp
M books/kestrel/c/language/.sys/ty...@useless-runes.lsp
M books/kestrel/c/language/.sys/val...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/vers...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/const-ast...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/const-...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/exec-stm...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/exec-stmt-w...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/pure-express...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/test...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/t...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-syn...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-s...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/ascii-id...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/code-en...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/disamb...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/external-pr...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/fi...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/forma...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/gra...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/implementatio...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/infer...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/input...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/langdef-map...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/langdef...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/le...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/macro-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/output...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/parser-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/parser...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/par...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/posi...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preprocesso...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/prepro...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preservable...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pri...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pur...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/rea...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/sp...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/stan...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/string...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/token-con...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/unamb...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/unicode-c...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/preprocessor-...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/prepro...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/vali...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/add-sectio...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/add-sect...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/constant-p...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/cop...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/proof-ge...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/ren...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/simp...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/speci...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/variables-in-co...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/wra...@useless-runes.lsp
M books/kestrel/c/transformation/command-line/.sys/wrap...@useless-runes.lsp
A books/kestrel/c/transformation/tests/add-section-attr/.sys/add-sect...@useless-runes.lsp
M books/kestrel/c/transformation/tests/free-vars/.sys/free...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/asg...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/asg-...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/b...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/blo...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/ca...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/cons...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/de...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/dow...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/g...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/glo...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/i...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/ife...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/log...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/lo...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/pa...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/pure-ex...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/retur...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/stmt...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/terna...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/un...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/vari...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/wh...@useless-runes.lsp
M books/kestrel/c/transformation/tests/subst-free/.sys/subst...@useless-runes.lsp
A books/kestrel/c/transformation/utilities/.sys/add-att...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/call-...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/collect...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/free...@useless-runes.lsp
A books/kestrel/c/transformation/utilities/.sys/qualifi...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/subst...@useless-runes.lsp
M books/kestrel/clause-processors/.sys/clause-to-...@useless-runes.lsp
M books/kestrel/clause-processors/.sys/handle-const...@useless-runes.lsp
M books/kestrel/clause-processors/.sys/simple-su...@useless-runes.lsp
M books/kestrel/crypto/aes/.sys/aes-...@useless-runes.lsp
M books/kestrel/crypto/attachments/.sys/kecca...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake-25...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blak...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/bla...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2s-exten...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/bla...@useless-runes.lsp
M books/kestrel/crypto/chacha/.sys/chac...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/.sys/deterministic-...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp256k1-dom...@useless-runes.lsp
M books/kestrel/crypto/keccak/.sys/keccak-t...@useless-runes.lsp
M books/kestrel/crypto/keccak/.sys/kec...@useless-runes.lsp
M books/kestrel/crypto/padding/.sys/pad-t...@useless-runes.lsp
M books/kestrel/crypto/padding/.sys/pad-t...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/baby-jubjub-s...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/bls12-3...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/bn-254-gr...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/ed25519-b...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/ed25519-g...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/goldilocks-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/jubjub-sub...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/koala...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/nist-p-256...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/nist-p-256-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/secp256k1-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/secp256k1-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/t...@useless-runes.lsp
M books/kestrel/crypto/r1cs/.sys/gad...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/example...@useless-runes.lsp
M books/kestrel/crypto/r1cs/gadgets/.sys/xor-...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/.sys/p1...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/.sys/rule...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/bit...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/na...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/range...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/x...@useless-runes.lsp
M books/kestrel/crypto/salsa/.sys/salsa2...@useless-runes.lsp
M books/kestrel/crypto/salsa/.sys/sal...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sha-3-va...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sh...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sup...@useless-runes.lsp
M books/kestrel/crypto/tea/.sys/inve...@useless-runes.lsp
M books/kestrel/crypto/tea/.sys/t...@useless-runes.lsp
A books/kestrel/data/.sys/d...@useless-runes.lsp
M books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/del...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/d...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/ins...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/benchmark/.sys/ran...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/co...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/d...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/heap-...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
M books/kestrel/data/utilities/.sys/li...@useless-runes.lsp
R books/kestrel/data/utilities/.sys/nat-...@useless-runes.lsp
R books/kestrel/data/utilities/.sys/n...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/t...@useless-runes.lsp
M books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/min...@useless-runes.lsp
M books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
M books/kestrel/data/utilities/total-order/.sys/total...@useless-runes.lsp
M books/kestrel/ethereum/.sys/data...@useless-runes.lsp
M books/kestrel/ethereum/.sys/mmp-...@useless-runes.lsp
M books/kestrel/ethereum/.sys/t...@useless-runes.lsp
M books/kestrel/ethereum/evm/.sys/e...@useless-runes.lsp
M books/kestrel/ethereum/evm/.sys/sup...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/baby-...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/blake2s-mi...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/r1cs-pro...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/read-bytes-...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/read-file-in...@useless-runes.lsp
M books/kestrel/floats/.sys/ieee-floats...@useless-runes.lsp
M books/kestrel/fty/.sys/any-n...@useless-runes.lsp
A books/kestrel/fty/.sys/byte-li...@useless-runes.lsp
M books/kestrel/fty/.sys/characte...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold-...@useless-runes.lsp
M books/kestrel/fty/.sys/deffo...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold-re...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold...@useless-runes.lsp
M books/kestrel/fty/.sys/defmake-s...@useless-runes.lsp
M books/kestrel/fty/.sys/defoma...@useless-runes.lsp
M books/kestrel/fty/.sys/string-str...@useless-runes.lsp
M books/kestrel/helpers/.sys/advice-imp...@useless-runes.lsp
A books/kestrel/helpers/.sys/defrul...@useless-runes.lsp
M books/kestrel/helpers/.sys/eval-...@useless-runes.lsp
M books/kestrel/java/atj/post-translation/.sys/fold-r...@useless-runes.lsp
M books/kestrel/java/language/.sys/hexadecim...@useless-runes.lsp
M books/kestrel/json-parser/.sys/parse...@useless-runes.lsp
M books/kestrel/jvm/.sys/array-b...@useless-runes.lsp
M books/kestrel/jvm/.sys/class-fi...@useless-runes.lsp
M books/kestrel/jvm/.sys/do-ins...@useless-runes.lsp
M books/kestrel/jvm/.sys/flo...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-f...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-r...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-...@useless-runes.lsp
M books/kestrel/jvm/.sys/j...@useless-runes.lsp
M books/kestrel/jvm/.sys/read-and-par...@useless-runes.lsp
A books/kestrel/lists-light/.sys/set-differen...@useless-runes.lsp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/meta/.sys/rewr...@useless-runes.lsp
M books/kestrel/meta/.sys/rewr...@useless-runes.lsp
M books/kestrel/number-theory/.sys/defprim...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/bv-r...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/prime-field...@useless-runes.lsp
M books/kestrel/simpl-imp/.sys/sema...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/static-sema...@useless-runes.lsp
M books/kestrel/syntheto/shallow/.sys/te...@useless-runes.lsp
M books/kestrel/terms-light/.sys/make-i...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/all-...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/decre...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/intege...@useless-runes.lsp
A books/kestrel/utilities/.sys/arith-fix-an...@useless-runes.lsp
A books/kestrel/utilities/.sys/arith-fix...@useless-runes.lsp
M books/kestrel/utilities/.sys/defstobj-...@useless-runes.lsp
M books/kestrel/utilities/.sys/for...@useless-runes.lsp
M books/kestrel/utilities/.sys/ld-hi...@useless-runes.lsp
M books/kestrel/utilities/.sys/redun...@useless-runes.lsp
M books/kestrel/utilities/.sys/run-json...@useless-runes.lsp
M books/kestrel/utilities/.sys/xdoc-...@useless-runes.lsp
M books/kestrel/x86/.sys/alt-...@useless-runes.lsp
M books/kestrel/x86/.sys/assumptions...@useless-runes.lsp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/.sys/assum...@useless-runes.lsp
M books/kestrel/x86/.sys/bytes-...@useless-runes.lsp
M books/kestrel/x86/.sys/canonical...@useless-runes.lsp
M books/kestrel/x86/.sys/condi...@useless-runes.lsp
M books/kestrel/x86/.sys/fl...@useless-runes.lsp
M books/kestrel/x86/.sys/flo...@useless-runes.lsp
M books/kestrel/x86/.sys/linear...@useless-runes.lsp
M books/kestrel/x86/.sys/memo...@useless-runes.lsp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-bytes-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-...@useless-runes.lsp
M books/kestrel/x86/.sys/readers-an...@useless-runes.lsp
M books/kestrel/x86/.sys/register-reader...@useless-runes.lsp
M books/kestrel/x86/.sys/register-reader...@useless-runes.lsp
M books/kestrel/x86/.sys/rfl...@useless-runes.lsp
A books/kestrel/x86/.sys/run-until...@useless-runes.lsp
R books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
R books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
A books/kestrel/x86/.sys/run-until...@useless-runes.lsp
M books/kestrel/x86/.sys/suppo...@useless-runes.lsp
M books/kestrel/x86/.sys/suppo...@useless-runes.lsp
M books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/sup...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/x86-c...@useless-runes.lsp
M books/kestrel/x86/.sys/z...@useless-runes.lsp
M books/kestrel/x86/tools/.sys/lifter-...@useless-runes.lsp
M books/kestrel/x86/tools/.sys/unroll-x8...@useless-runes.lsp
M books/kestrel/yul/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/yul/language/.sys/dynamic-...@useless-runes.lsp
M books/kestrel/yul/language/.sys/le...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-safe...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/dead-code-elimi...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/no-function-def...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/renaming-varia...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/renaming-var...@useless-runes.lsp
M books/kestrel/zcash/.sys/jub...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-add...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-hash-b...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-hash-inje...@useless-runes.lsp
M books/kestrel/zcash/.sys/peders...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-1-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/proof-...@useless-runes.lsp
R books/misc/character-encoding-test.acl2
A books/misc/character-encoding-test.acl2.moved
M books/misc/character-encoding-test.lisp
M books/projects/aleo/bft/next/.sys/author-round-pai...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/commi...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-previ...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-signer-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-sign...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsed-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsemen...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/initial...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposal-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-autho...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-a...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-d...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-endors...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-en...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-pre...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-roun...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/signed-i...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/signed-p...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/system...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/unequiv...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/unequivoca...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/validato...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2s-one-rou...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2s-sp...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2s1...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/keccak2...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/sup...@useless-runes.lsp
M books/projects/aleo/vm/circuits/library-extensions/.sys/om...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/boolean-a...@useless-runes.lsp
M books/projects/aleo/vm/language/early-version/.sys/par...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/bls12-377-...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/bls12-3...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/edwards-bls12-37...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/t...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/h...@useless-runes.lsp
A books/projects/hol-in-acl2/acl2/.sys/hpp...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/lem...@useless-runes.lsp
R books/projects/hol-in-acl2/acl2/.sys/set-of-h...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/te...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/theo...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/eval-po...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/eval-pol...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/eval-p...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/ex1-...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/ex1...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/ex1...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/example...@useless-runes.lsp
M books/projects/oracle/stv-invariant-extraction-pitfall/.sys/a...@useless-runes.lsp
M books/projects/pfcs/.sys/abstract-synt...@useless-runes.lsp
M books/projects/pfcs/.sys/abstract-s...@useless-runes.lsp
M books/projects/pfcs/.sys/convenience-...@useless-runes.lsp
M books/projects/pfcs/.sys/gra...@useless-runes.lsp
M books/projects/pfcs/.sys/lif...@useless-runes.lsp
M books/projects/pfcs/.sys/proof-...@useless-runes.lsp
M books/projects/pfcs/.sys/r1cs-...@useless-runes.lsp
M books/projects/pfcs/.sys/r1cs-...@useless-runes.lsp
M books/projects/pfcs/.sys/sema...@useless-runes.lsp
M books/projects/pfcs/.sys/toke...@useless-runes.lsp
M books/projects/pfcs/.sys/well-fo...@useless-runes.lsp
M books/projects/poseidon/.sys/ingonya...@useless-runes.lsp
M books/projects/poseidon/.sys/instant...@useless-runes.lsp
M books/projects/rac/lisp/.sys/expand-r...@useless-runes.lsp
M books/projects/rp-rewriter/.sys/cl-co...@useless-runes.lsp
M books/projects/rp-rewriter/.sys/eval-fu...@useless-runes.lsp
M books/projects/rp-rewriter/.sys/extract...@useless-runes.lsp
M books/projects/rp-rewriter/.sys/rp-th...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/casesplit-f...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/casesp...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/cons-to-...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/equal...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/fast-alist...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/hons-ac...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/hons-g...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/mv-nt...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/apply-bind...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/apply-me...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/eval-funct...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/ex-counter...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/extract-for...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/gua...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/match-lh...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/proof-func...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/rp-co...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/rp-equa...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/rp-rw-...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/rp-state-fun...@useless-runes.lsp
M books/projects/set-theory/.sys/can...@useless-runes.lsp
M books/projects/set-theory/.sys/fin...@useless-runes.lsp
M books/projects/set-theory/.sys/fo...@useless-runes.lsp
M books/projects/set-theory/.sys/injecti...@useless-runes.lsp
M books/projects/set-theory/.sys/inv...@useless-runes.lsp
M books/projects/set-theory/.sys/ordi...@useless-runes.lsp
M books/projects/set-theory/.sys/rest...@useless-runes.lsp
M books/projects/set-theory/.sys/schroeder-ber...@useless-runes.lsp
M books/projects/set-theory/.sys/set-a...@useless-runes.lsp
A books/projects/set-theory/.sys/sko...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/three-byte-op...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/two-byte-opc...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/em...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/log...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/move...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/move...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/pa...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/pa...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/pc...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/pm...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/pm...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/psh...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/ps...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/pun...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/rotate-a...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/fp/.sys/log...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/fp/.sys/simd-i...@useless-runes.lsp
M books/projects/x86isa/proofs/zeroCopy/marking-view/.sys/zero...@useless-runes.lsp
A books/std/basic/.sys/yyy...@useless-runes.lsp
M books/std/obags/.sys/co...@useless-runes.lsp
A books/std/omaps/.sys/as...@useless-runes.lsp
A books/std/omaps/.sys/compa...@useless-runes.lsp
M books/std/omaps/.sys/co...@useless-runes.lsp
A books/std/omaps/.sys/del...@useless-runes.lsp
A books/std/omaps/.sys/extensi...@useless-runes.lsp
A books/std/omaps/.sys/from-...@useless-runes.lsp
A books/std/omaps/.sys/from-...@useless-runes.lsp
A books/std/omaps/.sys/sub...@useless-runes.lsp
A books/std/omaps/.sys/upd...@useless-runes.lsp
M books/std/omaps/.sys/with-fixin...@useless-runes.lsp
M books/std/strings/.sys/bin-digit-...@useless-runes.lsp
M books/std/strings/.sys/dec-digit-...@useless-runes.lsp
M books/std/strings/.sys/hex-digit-...@useless-runes.lsp
M books/std/strings/.sys/oct-digit-...@useless-runes.lsp
A books/std/system/.sys/impl...@useless-runes.lsp
M books/std/util/.sys/add-io-pairs...@useless-runes.lsp
M books/std/util/.sys/add-io-pairs...@useless-runes.lsp
M books/std/util/.sys/add-io-pair...@useless-runes.lsp
M books/std/util/.sys/add-io-pa...@useless-runes.lsp
M books/std/util/tests/.sys/defagg...@useless-runes.lsp
M books/std/util/tests/.sys/def...@useless-runes.lsp
M books/system/apply/.sys/apply...@useless-runes.lsp
M books/system/doc/acl2-doc-wrap.lisp
M books/system/doc/acl2-doc.lisp
M books/system/doc/render-doc.lisp
A books/tools/.sys/elide-e...@useless-runes.lsp
A books/tools/.sys/elide...@useless-runes.lsp
A books/tools/.sys/eval-events-...@useless-runes.lsp
A books/tools/.sys/eval-events-f...@useless-runes.lsp
A books/tools/.sys/eval-event...@useless-runes.lsp
M books/tools/.sys/with-su...@useless-runes.lsp
M books/workshops/2020/peng-greenstreet/.sys/eval...@useless-runes.lsp
M books/workshops/2020/sswords-rewriter/.sys/sup...@useless-runes.lsp
M books/workshops/2020/sumners/.sys/gl-s...@useless-runes.lsp
M books/workshops/2023/coglio-mccarthy-smith/.sys/pf...@useless-runes.lsp
M books/workshops/2025/manjrekar/.sys/ctv...@useless-runes.lsp
M books/xdoc/.sys/save-c...@useless-runes.lsp
M boot-strap-pass-2-a.lisp
M boot-strap-pass-2-b.lisp
M defpkgs.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M doc/home-page.lisp
M doc/write-acl2-code-size.lisp
M emacs/acl2-doc-open-url.el
M emacs/acl2-doc.el
M emacs/emacs-acl2.el
M emacs/html-to-xdoc.el
M emacs/monitor.el
M float-a.lisp
M float-b.lisp
M float-raw.lisp
M futures-raw.lisp
M history-management.lisp
M hons-raw.lisp
M hons.lisp
M induct.lisp
M init.lisp
M interface-raw.lisp
M ld.lisp
M linear-a.lisp
M linear-b.lisp
M memoize-raw.lisp
M memoize.lisp
M multi-threading-raw.lisp
M new.html
M non-linear.lisp
M openmcl-acl2-trace.lisp
M other-events.lisp
M other-processes.lisp
M parallel-raw.lisp
M parallel.lisp
M proof-builder-a.lisp
M proof-builder-b.lisp
M proof-builder-pkg.lisp
M prove.lisp
M rewrite.lisp
M save-gprof.lsp
M serialize-raw.lisp
M serialize.lisp
M simplify.lisp
M tau.lisp
M translate.lisp
M type-set-a.lisp
M type-set-b.lisp

Log Message:
-----------
Merge.


Commit: b7846a2606f94a4fb6557495e42b979eba3fe77e
https://github.com/acl2/acl2/commit/b7846a2606f94a4fb6557495e42b979eba3fe77e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-23 (Mon, 23 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
A books/kestrel/c/proof-support/exec-expr-pure-list-openers.lisp
M books/kestrel/c/proof-support/top.lisp

Log Message:
-----------
[C] Move some rules to proof support.


Commit: bd7dd7b5c047661a14577235751e20d6b700bcf5
https://github.com/acl2/acl2/commit/bd7dd7b5c047661a14577235751e20d6b700bcf5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-23 (Mon, 23 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp

Log Message:
-----------
Merge.


Commit: b3cd821a6f11f1f8440f02d81570232051282563
https://github.com/acl2/acl2/commit/b3cd821a6f11f1f8440f02d81570232051282563
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-23 (Mon, 23 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
A books/kestrel/c/proof-support/exec-expr-pure-list-openers.lisp
M books/kestrel/c/proof-support/top.lisp

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/7c2812ccb07e...b3cd821a6f11

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[Alessandro Coglio]

Branch: refs/heads/testing