250 | 250 |
(format t "~& ~20Trewrite <term> using equations as rewerite rules")
|
251 | 251 |
(format t "~& ~20Toptional <Modexp> specifies the context")
|
252 | 252 |
(format t "~& exec [in <Modexp> : ] <term> .")
|
253 | |
(format t "~& exec+ [in <Modexp> : ] <term> .")
|
|
253 |
;; (format t "~& exec+ [in <Modexp> : ] <term> .")
|
254 | 254 |
(format t "~& ~20Trewrite <term> using both equations and rules")
|
255 | 255 |
(format t "~& ~20Toptional <Modexp> specifies the context")
|
256 | 256 |
(format t "~& parse [in <Modexp> : ] <term> .")
|
257 | 257 |
(format t "~& ~20Tparse <term>, print out the result")
|
258 | |
(format t "~& test {reduction|execution} <term> :expect <term> . ")
|
259 | |
(format t "~& ~20Tdo test reduction(execution) in the current context")
|
|
258 |
;; (format t "~& test {reduction|execution} <term> :expect <term> . ")
|
|
259 |
;; (format t "~& ~20Tdo test reduction(execution) in the current context")
|
260 | 260 |
;; (format t "~& rew limit {<number>| .}")
|
261 | 261 |
;; (format t "~& ~20Tset(unset) max number of rewriting")
|
262 | 262 |
;; (format t "~& stop at [<term>] .")
|
|
276 | 276 |
(format t "~& save <file>~20Tsave current definitions of modules to <file>")
|
277 | 277 |
(format t "~& restore <file>~20Trestore definitions of modules from <file>")
|
278 | 278 |
(format t "~& reset ~20Trecover defintions of built-in modules and standard prelude")
|
279 | |
(format t "~& full-reset~20Treset system to initial status")
|
|
279 |
(format t "~& full reset~20Treset system to initial status")
|
280 | 280 |
(format t "~&-- misc. commands")
|
281 | 281 |
(format t "~& clean memo ~20T clean up term memoization table")
|
282 | 282 |
(format t "~& dribble {<file>| .}~20T if <file> is given, begins to record the interaction")
|