Safe Haskell	None
Language	Haskell2010

Language.PTS.WHNF

Synopsis

Documentation

class WHNF t where Source #

Weak-head normal form.

>>> prettyPut $ whnf (lambdaStarIdentity @@ "Bool" @@ "True" :: Term LambdaStar)
True

Note: the evaluation proceeds even for ill-typed terms:

>>> prettyPut $ whnf (lambdaStarIdentity @@ "Int" @@ "True" :: Term LambdaStar)
True

TODO: Othen than App/Lam pairs

Minimal complete definition

Methods

whnf :: t s a -> t s a Source #

Instances

WHNF TermChk Source #
Instance details Defined in Language.PTS.WHNF Methods whnf :: TermChk s a -> TermChk s a Source #
WHNF TermInf Source #
Instance details Defined in Language.PTS.WHNF Methods whnf :: TermInf s a -> TermInf s a Source #