K

type TyName

type ValName

data Ty

data Val

data AnnVal

data Decl

data Tm

rTm1

rTm

rDecl1

rDecl

rAnnVal1

rAnnVal

rVal1

rVal

rTy1

rTy

x

y

z

a

b

c

type Delta

type Gamma

data Ctx

emptyCtx

checkTyVar

lookupTmVar

extendTy

extendTys

extendTm

extendTms

tcty

typecheckVal

typecheckAnnVal

typecheckDecl

typecheck

mkSubst

step

evaluate