Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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 :: 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

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