C

type TyName

type TmName

type ValName

data Ty

data Val

data AnnVal

data Decl

data Tm

data Heap

rTm1

rTm

rDecl1

rDecl

rAnnVal1

rAnnVal

rVal1

rVal

rTy1

rTy

mkTyApp

mkProd

x

y

z

a

b

c

type Delta

type Gamma

data Ctx

emptyCtx

checkTyVar

lookupTmVar

extendTy

extendTys

extendTm

extendTms

extendDecl

tcty

typecheckVal

typecheckAnnVal

typecheckDecl

typecheck

heapvalcheck

hoistcheck

mkSubst

step

evaluate

displayCode