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

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

KnownBool 'True Source # 
Instance details

Defined in Agda.Utils.TypeLits

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