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

Safe Haskell | Safe-Inferred
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 :: SBool b -> Bool
- class KnownBool (b :: Bool) where
  - boolSing :: SBool b
- boolVal :: forall proxy b. 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 :: 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 #