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

Agda.TypeChecking.Level

Synopsis

Documentation

data LevelKit

Constructors

LevelKit 

requireLevels :: TCM LevelKit

Raises an error if no level kit is available.