Idris.Core.TT

data FC

data FC'

data NameOutput

data TextFormatting

data OutputAnnotation

data ErrorReportPart

data Err' t

type Err

type TC

data Name

data SpecialName

type Ctxt a

lookupCtxtExact

data IntTy

data Const

data Raw

data Binder b

data UExp

data UConstraint

type UCs

data TT n

class TermSize a

type EnvTT n

data Datatype n

A few handy operations on well typed terms:

type Term

type Type

type Env

data WkEnvTT n

type WkEnv