ModuleAgda-2.8.0.2Haskell2010

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.

Synopsis

data WithDefault'
type WithDefault
value setDefault
value mapValue
value collapseDefault
value lensCollapseDefault
value lensKeepDefault

PackageAgda-2.8.0.2
Exports7
LanguageHaskell2010
LicenceMIT
SourceWithDefault.hs

datadata WithDefault' a (b :: Bool)

Source#

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

Default
Value !a

Instances5Eq, Show, NFData, Null, EmbPrj

Eq a => Eq (WithDefault' a b)Defined in Agda-2.8.0.2 · Agda.Utils.WithDefault
Show a => Show (WithDefault' a b)Defined in Agda-2.8.0.2 · Agda.Utils.WithDefault
NFData (WithDefault' a b)Defined in Agda-2.8.0.2 · Agda.Utils.WithDefault
Null (WithDefault' a b)Defined in Agda-2.8.0.2 · Agda.Utils.WithDefault
The null value of 'WithDefault b' is Default.
(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

typetype WithDefault (b :: Bool) = WithDefault' Bool b

valuesetDefault :: Boolean a => a -> WithDefault' a b -> WithDefault' a b

Source#

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.

valuemapValue :: Boolean a => (a -> a) -> WithDefault' a b -> WithDefault' a b

Source#

Only modify non-Default values.

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

Source#

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.

valuelensCollapseDefault :: (Boolean a, KnownBool b) => Lens' (WithDefault' a b) a

Source#

Focus, overwriting Default.

valuelensKeepDefault :: (Boolean a, Eq a, KnownBool b) => Lens' (WithDefault' a b) a

Source#

Update, but keep Default when new value is default value.