Agda-2.6.4.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

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.

Constructors

Default 
Value !a 

Instances

Instances details
(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Null (WithDefault' a b) Source #

The null value of 'WithDefault b' is Default.

Instance details

Defined in Agda.Utils.WithDefault

Show a => Show (WithDefault' a b) Source # 
Instance details

Defined in Agda.Utils.WithDefault

NFData (WithDefault' a b) Source # 
Instance details

Defined in Agda.Utils.WithDefault

Methods

rnf :: WithDefault' a b -> () #

Eq a => Eq (WithDefault' a b) Source # 
Instance details

Defined in Agda.Utils.WithDefault

Methods

(==) :: WithDefault' a b -> WithDefault' a b -> Bool #

(/=) :: WithDefault' a b -> WithDefault' a b -> Bool #

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.