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

Safe HaskellSafe
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
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 #