Idris2Doc : JS.Undefined

JS.Undefined

(source)

Definitions

data Undefined : Type
Totality: total
Visibility: export
Hints:
Eq Undefined
FromFFI Undefined Undefined
SafeCast Undefined
Show Undefined
ToFFI Undefined Undefined
undefined : Undefined
  The `undefined` constant
isUndefined : a -> Bool
  Tests, whether a value of questionable origin is undefined

Totality: total
Visibility: export
data UndefOr : Type -> Type
Totality: total
Visibility: export
Hints:
FromFFI a b => FromFFI (Optional a) (UndefOr b)
SafeCast a => SafeCast (UndefOr a)
ToFFI a b => ToFFI (Optional a) (UndefOr b)
undef : UndefOr a
Totality: total
Visibility: export
def : a -> UndefOr a
Totality: total
Visibility: export
data Optional : Type -> Type
Totality: total
Visibility: public export
Constructors:
Undef : Optional a
Def : a -> Optional a

Hints:
Alternative Optional
Applicative Optional
Eq a => Eq (Optional a)
Foldable Optional
FromFFI a b => FromFFI (Optional a) (UndefOr b)
Functor Optional
Monad Optional
Ord a => Ord (Optional a)
Show a => Show (Optional a)
ToFFI a b => ToFFI (Optional a) (UndefOr b)
Traversable Optional
optional : Lazy b -> (a -> b) -> Optional a -> b
Totality: total
Visibility: public export
fromOptional : Lazy a -> Optional a -> a
Totality: total
Visibility: public export
optionalToUndefOr : Optional a -> UndefOr a
Totality: total
Visibility: export
optUp : {auto 0 {conArg:5464} : JSType a} -> Optional a -> {auto 0 _ : Elem b (Types a)} -> UndefOr b
Totality: total
Visibility: export
omyUp : {auto 0 {conArg:5500} : JSType a} -> Optional (Maybe a) -> {auto 0 _ : Elem b (Types a)} -> UndefOr (Nullable b)
Totality: total
Visibility: export
maybeToOptional : Maybe a -> Optional a
Totality: total
Visibility: public export
optionalToMaybe : Optional a -> Maybe a
Totality: total
Visibility: public export
undeforToOptional : UndefOr a -> Optional a
Totality: total
Visibility: export
undeforToMaybe : UndefOr a -> Maybe a
Totality: total
Visibility: export