		Search-engine friendly clone of the ACL2 documentation.

Developers-guide-background

Developers-guide-background-extra

Some Implementation Background Extra Information

Here is a call tree built bottom-up when exploring how thm-fn calls the rewriter, which is an exercise suggested in the section, developers-guide-background. There are a few extra nodes in this tree, obtained by looking for callers of rewrite and of prove.

rewrite
  rewrite-atm
    rewrite-clause, rewrite-clause-lst
      simplify-clause1
        simplify-clause
          waterfall-step1
            waterfall-step
              waterfall0
                waterfall1
                  waterfall
                    prove-loop2
                      prove-loop1
                        prove-loop0
                          prove-loop
                            prove
                              prove-termination
                              prove-guard-clauses
                              #+:non-standard-analysis verify-valid-std-usage
                              prove-corollaries1
                              defthm-fn1
                                defthm-fn
                              thm-fn
                              prove-defattach-guards1
                              prove-defattach-constraint
                            pc-prove
  mfc-rw-raw
  pc-rewrite*-1