A

type TyName

type ValName

data Flag

data Ty

data Val

data Ann v

data Decl

data Tm

data HeapVal

data Heap

rTm1

rTm

rDecl1

rDecl

rAnn1

rAnn

rVal1

rVal

rTy1

rTy

rFlag1

rFlag

rHeapVal1

rHeapVal

mkTyApp

lets

x

y

z

a

b

c

type Delta

type Gamma

data Ctx

emptyCtx

checkTyVar

lookupTmVar

extendTy

extendTys

extendTm

extendTms

tcty

typecheckHeapVal

typecheckVal

typecheckAnnVal

typecheckDecl

typecheck

progcheck