Data.Syntactic.Functional

Syntactic constructs

data Name

data Construct sig

data Binding sig

maxLam

lam

fromDeBruijn

data BindingT sig

maxLamT

lamT

class BindingDomain sym

data MONAD m sig

data Remon sym m a

desugarMonad

Alpha-equivalence

type AlphaEnv

alphaEq'

alphaEq

Evaluation

type family Denotation sig

class Eval s

evalDen

type family DenotationM m sig

liftDenotationM

type RunEnv

class EvalEnv sym env

compileSymDefault

evalOpen

evalClosed

Well-scoped terms

class Ext ext orig

lookEnv

data BindingWS sig

lamWS

evalOpenWS

evalClosedWS

type family LiftReader env sig

type family UnReader a

type family LowerReader sig

data ReaderSym sym sig

type WS sym env a

fromWS

smartWS