Re: [stack] disallowing recursive definitions

On Feb 28, 2008, at 3:39 PM, John Nowak wrote:

> 6. It becomes possible to prove termination when using recursive
> combinators that always terminate given that their arguments always
> terminate (such as primrec).

To clarify, this is possible with recursive definitions as well.  
Without them however, it's a trivial addition to the type system that  
works exactly the same way that tracking of side effects works.

- John