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

Agda.TypeChecking.Level

Synopsis

Documentation

data LevelKit Source

Constructors

LevelKit 

requireLevels :: TCM LevelKitSource

Raises an error if no level kit is available.