HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.WithDefault

Potentially uninitialised Booleans.

The motivation for this small library is to distinguish between a boolean option with a default value and an option which has been set to what happens to be the default value. In one case the default can be overriden (e.g. --cubical implies --without-K) while in the other case the user has made a mistake which they need to fix.

  • 2 types
  • 5 values
  • PackageAgda-2.7.0.1
  • Exports7
  • LanguageHaskell2010
  • LicenceMIT
  • SourceWithDefault.hs
datadata WithDefault' a (b :: Bool)
#

We don't want to have to remember for each flag whether its default value is True or False. So we bake it into the representation: the flag's type will mention its default value as a phantom parameter.

Constructors

Instances5Eq, Show, NFData, Null, EmbPrj
valuesetDefault :: Boolean a => a -> WithDefault' a b -> WithDefault' a b
#

The main mode of operation of these flags, apart from setting them explicitly, is to toggle them one way or the other if they hadn't been set already.

valuecollapseDefault :: (Boolean a, KnownBool b) => WithDefault' a b -> a
#

Provided that the default value is a known boolean (in practice we only use True or False), we can collapse a potentially uninitialised value to a boolean.