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

Safe Haskell | Safe
Language | Haskell2010

Agda.Utils.WithDefault

Description

Potentially uninitialised Booleans

# Documentation

data WithDefault (b :: Bool) Source #

Constructors

Default |
Value Bool |

Instances

Eq (WithDefault b) Source # |
Instance details Defined in Agda.Utils.WithDefault Methods (==) :: WithDefault b -> WithDefault b -> Bool Source # (/=) :: WithDefault b -> WithDefault b -> Bool 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 #
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 #

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

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