Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Level

Synopsis

Documentation

newtype LevelView

Constructors

Max [PlusView] 

Instances

data LevelKit

Constructors

LevelKit 

levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)

requireLevels :: TCM LevelKit

Raises an error if no level kit is available.

levelView :: MonadTCM tcm => Term -> tcm LevelView