Agda.Utils.TypeLits

Type level literals, inspired by GHC.TypeLits.

Documentation

data SBool (b :: Bool) where

Singleton for type level booleans.

Constructors

STrue :: SBool 'True

SFalse :: SBool 'False

eraseSBool :: forall (b :: Bool). SBool b -> Bool

class KnownBool (b :: Bool) where

A known boolean is one we can obtain a singleton for. Concrete values are trivially known.

Methods

boolSing :: SBool b

Instances

KnownBool 'False

Defined in Agda.Utils.TypeLits

Methods

boolSing :: SBool 'False

KnownBool 'True

Defined in Agda.Utils.TypeLits

Methods

boolSing :: SBool 'True

boolVal :: forall proxy (b :: Bool). KnownBool b => proxy b -> Bool