how do I define WHNF in words. who has done it before that I can copy from

Sacchini uses it but doesn't define it :dragnyell:


The problem is that a fixpoint in WHNF necessarily must have arguments in WHNF to ensure that the fixpoint does not reduce any further, which goes against the idea that a term is in WHNF if the head (fixpoint) is irreducible (fixpoints don't reduce, naturally)

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.