Abt.Tutorial

data M α

runM

data Lang ns

lam

app

ax

unit

pi

data StepT m α

stepsExhausted

step

star

eval

data JudgeT m α

type Ctx

raise

checkTy

inferTy

identityTm

appTm

main