Head Normal Form definition theory, reduction
(HNF) A term describing a lambda expression
whose top level is either a variable, a data value, a built-in function applied to too few arguments, or a lambda abstraction
whose body is not reducible. I.e. the top level is neither a redex
nor a lambda abstraction with a reducible body.
An expression in HNF may contain redexes in argument postions whereas a normal form
Compare Weak Head Normal Form