Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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 :: 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

boolSing :: SBool b Source #

Instances

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. KnownBool b => proxy b -> Bool Source #