Agda-2.6.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.WithDefault

Description

Potentially uninitialised Booleans

Documentation

data WithDefault (b :: Bool) Source #

Constructors

Default 
Value Bool 

Instances

Instances details
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 #