cd ~moore
have firefox with the combined xdoc in it
v74
; start here:

(quote terms)
(trans '(+ 1 x y))
(pe '*maximum-positive-32-bit-integer*)
(trans '(+ *maximum-positive-32-bit-integer* x))

(trans '(cond (p (cadr x)) (q (cddr x))(t x)))
(trans1 '(cond (p (cadr x)) (q (cddr x))(t x)))
(value :q)
(macroexpand '(cond (p (cadr x)) (q (cddr x))(t x)))
(lp)

(trans '(let ((x a)(y b)) (+ x y z)))
(trans '(let* ((x a)(y b)) (+ x y z)))
(trans '(implies (and a b) c))

(quote clauses)
(clausify '(if (if a b 'NIL) c 'T) nil nil nil)
(clausify '(if (if a 'T b) c 'T) nil nil nil)

(thm (iff (implies (or (and a1 a2) (and b1 b2)) (and c1 c2))
          (if (if (if a1 a2 'NIL) 'T (if b1 b2 'NIL)) (if c1 c2 'NIL) 'T)))

(clausify '(if (if (if a1 a2 'NIL) 'T (if b1 b2 'NIL)) (if c1 c2 'NIL) 'T) nil nil nil)

(quote world)

(length (w state))

(walkabout (w state) state)

(defun ap (x y)
  (if (endp x)
      y
      (cons (car x)
            (ap (cdr x) y))))

(walkabout (w state) state)

(props 'ap)

(value :q)
(symbol-plist 'ap)
(lp)

(getpropc 'ap 'formals nil (w state))
(getpropc 'ap 'typo 'default (w state))
(getpropc 'ap 'type-prescriptions nil (w state))

(quote (tags search for 'type-prescriptions looking for uses of the property))

(quote (meta-dot type-set-with-rules))
(quote (meta-dot type-prescription))

(quote (follow defun down into defuns-fn1 to see putprops and update-w and point out the typical pattern))

(quote (TABLE should have been named DEF-TABLE!  Find acl2-defaults-table))

(quote (meta-dot *acl2-exports* and remember books/misc/check-acl2-exports.lisp))

(quote (global variables -- of state and of world))

(global-val 'command-landmark (w state))

(get-global 'acl2-version state)

(f-get-global 'acl2-version state)

(trans '(f-get-global 'acl2-version state))

(value :q)
(macroexpand '(f-get-global 'acl2-version state))
(lp)

(quote (search for Essay on Tag))

(quote (search for Essay on Enabl))

(quote (meta-dot enabled-structure))


(quote errors)

(er soft 'demo "It's bad to see ~x0!" 123)

(quote (see doc er))

(quote (meta-dot chk-acceptable-defuns1))

(quote (

Write a function that does not have access
to STATE but checks that every element of
a list is a number and generates a nice error
message otherwise.  Then define a wrapper
with STATE to cause the error.

))


(defun chk-numbers (x i)
  (cond ((endp x) nil)
        ((acl2-numberp (car x))
         (chk-numbers (cdr x) (+ 1 i)))
        (t (msg "the ~n0 (zero-based) element, ~
                 which is ~x1, is not a number!"
                (list i) (car x)))))
(defun chk-numbers-wrapper (x state)
  (declare (xargs :mode :program
                  :stobjs (state)))
  (let ((msg (chk-numbers x 0)))
    (cond
     (msg (er soft 'foo
              "This is a bad list because ~@0"
              msg))
     (t (value t)))))

(chk-numbers-wrapper '(29 33 16 13 40 782 98) state)

(chk-numbers-wrapper '(29 33 16 13 TOMMY 782 98) state)

(chk-numbers-wrapper '(29 33 1 2 23 4 5 6 7 8
                          0 1 2 3 4 5 6 7 8 9
                          0 1 2 3 4 5 6 7 8 9
                          0 1 2 3 4 5 6 7 8 9
                          TOMMY
                          782 98) state)