derivation-trees-0.7.1: DerivationTrees/ManualPTS.hs

module DerivationTrees.ManualPTS where

import DerivationTrees
import DerivationTrees.Basics
import Data.List

assert env val typ = tex "Assert" [mconcat $ intersperse (TeX ",") env,val,typ]
(-:) var typ = brace var <> tex "IS" [] <> brace typ

lam   binding body    = tex "LAMBDA" [binding, body]
pi    binding body    = tex "FORALL" [binding, body]
subs  term var s      = tex "SUBS" [term,var,s]
($$)   fun arg      = tex "APP" [fun, arg]
tso s = tex "tsort" [s]
many x = tex "many" [x]
x --> y = brace x <> tex "to" [mempty] <> brace y