Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.WithDefault

Description

Potentially uninitialised Booleans

# Documentation

data WithDefault (b :: Bool) Source #

Constructors

Default |
Value !Bool |

#### Instances

Instances details

Typeable b => EmbPrj (WithDefault b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithDefault b -> S Int32 Source # icod_ :: WithDefault b -> S Int32 Source # value :: Int32 -> R (WithDefault b) Source #
Show (WithDefault b) Source # |
Instance details Defined in Agda.Utils.WithDefault Methods showsPrec :: Int -> WithDefault b -> ShowS Source # show :: WithDefault b -> String Source # showList :: [WithDefault b] -> ShowS Source #
NFData (WithDefault b) Source # |
Instance details Defined in Agda.Utils.WithDefault Methods rnf :: WithDefault b -> () Source #
Eq (WithDefault b) Source # |
Instance details Defined in Agda.Utils.WithDefault Methods (==) :: WithDefault b -> WithDefault b -> Bool Source # (/=) :: WithDefault b -> WithDefault b -> Bool Source #

setDefault :: Bool -> WithDefault b -> WithDefault b Source #

collapseDefault :: KnownBool b => WithDefault b -> Bool Source #