let is_redex (t:term):bool = not (t = reduce_one_step t)
-let rec reduce_eager (t:term):term = match t with
+let rec reduce (t:term):term = match t with
I -> I
| K -> K
| S -> S
| FA (a, b) ->
- let t' = FA (reduce_eager a, reduce_eager b) in
- if (is_redex t') then reduce_eager (reduce_one_step t')
+ let t' = FA (reduce a, reduce b) in
+ if (is_redex t') then reduce (reduce_one_step t')
else t'
let rec reduce_lazy (t:term):term = match t with