Safe Haskell	None
Language	Haskell2010

Agda.Utils.TypeLits

Description

Type level literals, inspired by GHC.TypeLits.

Synopsis

Documentation

data SBool (b :: Bool) where Source #

Singleton for type level booleans.

Constructors

STrue :: SBool 'True
SFalse :: SBool 'False

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

class KnownBool (b :: Bool) where Source #

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

Methods

Instances details

KnownBool 'False Source #
Instance details Defined in Agda.Utils.TypeLits Methods boolSing :: SBool 'False Source #
KnownBool 'True Source #
Instance details Defined in Agda.Utils.TypeLits Methods boolSing :: SBool 'True Source #

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