Safe Haskell | None |
---|---|
Language | Haskell2010 |
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' a (b :: Bool)
- type WithDefault (b :: Bool) = WithDefault' Bool b
- setDefault :: forall a (b :: Bool). Boolean a => a -> WithDefault' a b -> WithDefault' a b
- mapValue :: forall a (b :: Bool). Boolean a => (a -> a) -> WithDefault' a b -> WithDefault' a b
- collapseDefault :: forall a (b :: Bool). (Boolean a, KnownBool b) => WithDefault' a b -> a
- lensCollapseDefault :: forall a (b :: Bool). (Boolean a, KnownBool b) => Lens' (WithDefault' a b) a
- lensKeepDefault :: forall a (b :: Bool). (Boolean a, Eq a, KnownBool b) => Lens' (WithDefault' a b) a
Documentation
data 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.
Instances
(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b) Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: WithDefault' a b -> S Int32 Source # icod_ :: WithDefault' a b -> S Int32 Source # value :: Int32 -> R (WithDefault' a b) Source # | |
Null (WithDefault' a b) Source # | The null value of 'WithDefault b' is |
Defined in Agda.Utils.WithDefault empty :: WithDefault' a b Source # null :: WithDefault' a b -> Bool Source # | |
NFData (WithDefault' a b) Source # | |
Defined in Agda.Utils.WithDefault rnf :: WithDefault' a b -> () | |
Show a => Show (WithDefault' a b) Source # | |
Defined in Agda.Utils.WithDefault showsPrec :: Int -> WithDefault' a b -> ShowS show :: WithDefault' a b -> String showList :: [WithDefault' a b] -> ShowS | |
Eq a => Eq (WithDefault' a b) Source # | |
Defined in Agda.Utils.WithDefault (==) :: WithDefault' a b -> WithDefault' a b -> Bool (/=) :: WithDefault' a b -> WithDefault' a b -> Bool |
type WithDefault (b :: Bool) = WithDefault' Bool b Source #
setDefault :: forall a (b :: Bool). 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.
mapValue :: forall a (b :: Bool). Boolean a => (a -> a) -> WithDefault' a b -> WithDefault' a b Source #
Only modify non-Default
values.
collapseDefault :: forall a (b :: Bool). (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.
lensCollapseDefault :: forall a (b :: Bool). (Boolean a, KnownBool b) => Lens' (WithDefault' a b) a Source #
Focus, overwriting Default
.
lensKeepDefault :: forall a (b :: Bool). (Boolean a, Eq a, KnownBool b) => Lens' (WithDefault' a b) a Source #
Update, but keep Default
when new value is default value.