Stepwise Reduction

In figure 2 is a short example for stepwise evaluation. As you can see, the redex is always underlined and if you want to evaluate the identifier to a value, simply pass the variable to the interpreter. Be aware that in transparent mode the output for complicated terms, e.g. a fixpoint computation, is in general very complex.

Figure 2: illustration of the stepping mode

- def inc = \x:Int.x+1;
> def inc = <fun> : Int->Int
- def s = inc (inc (if 3+1<=4 then 2 else ~1));
> def s = inc (inc (if 3+1<=4 then 2 else ~1)) : Int
                       ^^^
- rstep s;
> def it = inc (inc (if 4<=4 then 2 else ~1)) : Int
                        ^^^^
- def s' = rstep;
> def s' = inc (inc (if true then 2 else ~1)) : Int
                     ^^^^^^^^^^^^^^^^^^^^^^
- rstep s';
> def it = inc (inc 2) : Int
                ^^^^^
- rstep;
> def it = inc (2+1) : Int
                ^^^
- it;
> def it = 4 : Int
-