Permalink
Browse files

Minor updates to CBV_CONV documentation.

  • Loading branch information...
1 parent 62751b8 commit 7322733ce8486b6dabc861bd83b4e4e7a3162ab8 @acjf3 acjf3 committed May 17, 2013
Showing with 10 additions and 10 deletions.
  1. +10 −10 help/Docfiles/computeLib.CBV_CONV.doc
@@ -9,7 +9,7 @@ Call by value rewriting.
compute
\DESCRIBE
-The conversion {CBV_CONV} expects an simplification set and a
+The conversion {CBV_CONV} expects a simplification set and a
term. Its term argument is rewritten using the equations added in the
simplification set. The strategy used is somewhat similar to ML's,
that is call-by-value (arguments of constants are completely reduced
@@ -64,14 +64,14 @@ rules needed for basic boolean and arithmetical calculations built in.
\EXAMPLE
{
- - val rws = new_compset [lazyfy_thm COND_CLAUSES];
+ - val rws = computeLib.new_compset [computeLib.lazyfy_thm COND_CLAUSES];
> val rws = <compset> : compset
- - CBV_CONV rws (--`(\x.x) ((\x.x) if T then 0+0 else 10)`--);
+ - computeLib.CBV_CONV rws ``(\x.x) ((\x.x) if T then 0+0 else 10)``;
> val it = |- (\x. x) ((\x. x) (if T then 0 + 0 else 10)) = 0 + 0 : thm
- - CBV_CONV (reduceLib.num_compset())
- (--`if 100 - 5 * 5 < 80 then 2 EXP 16 else 3`--);
+ - computeLib.CBV_CONV (reduceLib.num_compset())
+ ``if 100 - 5 * 5 < 80 then 2 EXP 16 else 3``;
> val it = |- (if 100 - 5 * 5 < 80 then 2 ** 16 else 3) = 65536 : thm
}
@@ -80,16 +80,16 @@ huge result, or even loop. The same may occur if the initial term to
reduce contains free variables.
{
val eqn = bossLib.Define `exp n p = if p=0 then 1 else n * (exp n (p-1))`;
- val _ = add_thms [eqn] computeLib.the_compset;
+ val _ = computeLib.add_thms [eqn] rws;
- - CBV_CONV rws (--`exp 2 n`--);
+ - computeLib.CBV_CONV rws ``exp 2 n``;
> Interrupted.
- - set_skip rws "COND" (SOME 1);
+ - computeLib.set_skip rws ``COND`` (SOME 1);
> val it = () : unit
- - CBV_CONV rws (--`exp 2 n`--);
- > val it = |- exp 2 n = (if n = 0 then 1 else 2 * exp 2 (n - 1)) : thm
+ - computeLib.CBV_CONV rws ``exp 2 n``;
+ > val it = |- exp 2 n = if n = 0 then 1 else 2 * exp 2 (n - 1) : thm
}
The first invocation of {CBV_CONV} loops since the exponent
never reduces to 0. Below the first steps are computed:

0 comments on commit 7322733

Please sign in to comment.