Libraries.Data.WithDefault

Definitions

data WithDefault : (0 a : Type) -> (0 _ : a) -> Type

Totality: total
Visibility: export
Constructors:

DefaultedValue : WithDefault a def

SpecifiedValue : a -> WithDefault a def

Hints:

Eq a => Eq (WithDefault a def)

Ord a => Ord (WithDefault a def)

Reflect a => Reflect (WithDefault a def)

Reify a => Reify (WithDefault a def)

TTC a => TTC (WithDefault a def)

specified : a -> WithDefault a def

Visibility: export

defaulted : WithDefault a def

Visibility: export

specifyValue : a -> WithDefault a def -> WithDefault a def

Visibility: export

replaceSpecified : WithDefault a def -> WithDefault a def'

Visibility: export

collapseDefault : WithDefault a def -> a

Visibility: export

onWithDefault : Lazy b -> (a -> b) -> WithDefault a def -> b

Visibility: export

collapseDefaults : Eq a => WithDefault a def -> WithDefault a def -> Either (a, a) a

Visibility: export

isDefaulted : WithDefault a def -> Bool

Visibility: export

isSpecified : WithDefault a def -> Bool

Visibility: export