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
A known boolean is one we can obtain a singleton for. Concrete values are trivially known.