Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K

Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.TypeLits

Type level literals, inspired by GHC.TypeLits.

Synopsis

data SBool
value eraseSBool
class KnownBool
value boolVal

PackageAgda-2.8.0.2
Exports4
LanguageHaskell2010
LicenceMIT
SourceTypeLits.hs

datadata SBool (b :: Bool) where

Singleton for type level booleans.

Constructors

STrue :: SBool 'True
SFalse :: SBool 'False

valueeraseSBool :: SBool b -> Bool

classclass KnownBool (b :: Bool) where

A known boolean is one we can obtain a singleton for. Concrete values are trivially known.

Methods

boolSing :: SBool b

Instances2KnownBool

KnownBool 'FalseDefined in Agda-2.8.0.2 · Agda.Utils.TypeLits
KnownBool 'TrueDefined in Agda-2.8.0.2 · Agda.Utils.TypeLits

valueboolVal :: KnownBool b => proxy b -> Bool