Andrew Walter

Oops, after fumbling around a bit more with `defpattern` and `guard` I managed to get something working: ``` (defpattern type-bind (ty var) (let ((it (gensym "WHATBIND"))) `(guard1 (,it :type ,ty)...

Oh wow, I didn't realize you could use `and` for this! I'll work on a PR to extend the `type` pattern definition as you describe it, and I'll also maybe...

This occurs without having a rebuild of ACL2 in between when the certification was performed and when the book is included. I think that rules out your guess above, but...

`:check-expansion t` did not fix the issue, but I was able to minimize the example to the following by looking at what `modify-raw-defun` expands into: ``` lisp (in-package "ACL2") (include-book...

Note that if you put ACL2 into program mode (e.g insert `(program)` right before the first `defun foo`), your attempt also results in an infinite loop. Similarly, if I remove...

Apologies for the extreme delay here. As Matt says, we're doing a bunch of hacky raw-Lisp stuff here so it's totally fair to consider this not to be an ACL2...

Apologies, yes, I'm talking about https://www.cs.utexas.edu/~moore/acl2/v8-5/HTML/installation/obtaining-and-installing.html. That is also the page to which I suggest adding a section on "ways to try ACL2 out".

Great idea - I strongly agree with moving as much content from the ["Obtaining and Installing" page](https://www.cs.utexas.edu/~moore/acl2/v8-5/HTML/installation/obtaining-and-installing.html) as possible into XDOC topics. I'd be happy to update those topics once...