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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.TypeLits

Description

Type level literals, inspired by GHC.TypeLits.

Synopsis

- data SBool (b :: Bool) where
  - STrue :: SBool 'True
  - SFalse :: SBool 'False
- eraseSBool :: forall (b :: Bool). SBool b -> Bool
- class KnownBool (b :: Bool) where
  - boolSing :: SBool b
- boolVal :: forall proxy (b :: Bool). KnownBool b => proxy b -> Bool

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