| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.WithDefault
Description
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 Methods 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 | |
| NFData (WithDefault' a b) Source # | |
Defined in Agda.Utils.WithDefault Methods rnf :: WithDefault' a b -> () | |
| Show a => Show (WithDefault' a b) Source # | |
Defined in Agda.Utils.WithDefault Methods 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 Methods (==) :: 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.