Control.Monad.Trans.Open.Example

Syntax

data Ty

data Tm

Judgement Forms

data J a

Theories

type Theory j

unitThy

prodThy

combinedThy

Result

judge

Injecting Effects

traceThy

data Pack φ

tracedJudge