Idris2Doc : Prelude.Types

# Prelude.Types

`  Decidability. A decidable property either holds or is a contradiction.`

Totality: total
Constructors:
Yes : prop -> Decprop
`  The case where the property holds.  @ prf the proof`
No : Notprop -> Decprop
`  The case where the property holding would be a contradiction.  @ contra a demonstration that prop would be a contradiction`
dataEither : Type -> Type -> Type
`  A sum type.`

Totality: total
Constructors:
Left : a -> Eitherab
`  One possibility of the sum, conventionally used to represent errors.`
Right : b -> Eitherab
`  The other possibility, conventionally used to represent success.`
dataMaybe : Type -> Type
`  An optional value. This can be used to represent the possibility of  failure, where a function may return a value, or not.`

Totality: total
Constructors:
Nothing : Maybety
`  No value stored`
Just : ty -> Maybety
`  A value of type `ty` is stored`
dataNat : Type
`  Natural numbers: unbounded, unsigned integers which can be pattern matched.`

Totality: total
Constructors:
Z : Nat
`  Zero.`
S : Nat -> Nat
`  Successor.`
interfaceRange : Type -> Type
Parameters: a
Constructor: MkRange
Methods:
rangeFromTo : a -> a -> Lista
rangeFromThenTo : a -> a -> a -> Lista
rangeFrom : a -> Streama
rangeFromThen : a -> a -> Streama

Implementations:
RangeNat
(Integrala, (Orda, Nega)) => Rangea
acos : Double -> Double
Totality: total
asin : Double -> Double
Totality: total
atan : Double -> Double
Totality: total
ceiling : Double -> Double
Totality: total
chr : Int -> Char
`  Convert the number to its backend dependent (usually Unicode) Char  equivalent.`

Totality: total
compareNat : Nat -> Nat -> Ordering
Totality: total
cos : Double -> Double
Totality: total
cosh : Double -> Double
Totality: total
count : Foldablet => (a -> Bool) -> ta -> Nat
`  Counts the number of elements that satify a predicate.`

Totality: total
countFrom : n -> (n -> n) -> Streamn
Totality: total
either : Lazy (a -> c) -> Lazy (b -> c) -> Eitherab -> c
`  Simply-typed eliminator for Either.  @ f the action to take on Left  @ g the action to take on Right  @ e the sum to analyze`

Totality: total
elem : Eqa => a -> Lista -> Bool
`  Check if something is a member of a list using the default Boolean equality.`

Totality: total
equalNat : Nat -> Nat -> Bool
Totality: total
euler : Double
Totality: total
exp : Double -> Double
Totality: total
fastConcat : ListString -> String
fastPack : ListChar -> String
fastUnpack : String -> ListChar
floor : Double -> Double
Totality: total
getAt : Nat -> Lista -> Maybea
`  Lookup a value at a given position`

Totality: total
`  The first element of an infinite stream.`

Totality: total
integerToNat : Integer -> Nat
Totality: total
isAlpha : Char -> Bool
`  Returns true if the character is in the ranges [A-Z][a-z].`

Totality: total
isAlphaNum : Char -> Bool
`  Returns true if the character is in the ranges [A-Z][a-z][0-9].`

Totality: total
isControl : Char -> Bool
`  Returns true if the character is a control character.`

Totality: total
isDigit : Char -> Bool
`  Returns true if the character is in the range [0-9].`

Totality: total
isHexDigit : Char -> Bool
`  Returns true if the character is a hexadecimal digit i.e. in the range  [0-9][a-f][A-F].`

Totality: total
isLower : Char -> Bool
`  Returns true if the character is in the range [a-z].`

Totality: total
isNL : Char -> Bool
`  Returns true if the character represents a new line.`

Totality: total
isOctDigit : Char -> Bool
`  Returns true if the character is an octal digit.`

Totality: total
isSpace : Char -> Bool
`  Returns true if the character is a whitespace character.`

Totality: total
isUpper : Char -> Bool
`  Returns true if the character is in the range [A-Z].`

Totality: total
log : Double -> Double
Totality: total
maybe : Lazy b -> Lazy (a -> b) -> Maybea -> b
Totality: total
minus : Nat -> Nat -> Nat
`  Subtract natural numbers. If the second number is larger than the first,  return 0.`

Totality: total
mult : Nat -> Nat -> Nat
`  Multiply natural numbers.`

Totality: total
natToInteger : Nat -> Integer
Totality: total
ord : Char -> Int
`  Return the backend dependent (usually Unicode) numerical equivalent of the Char.`

Totality: total
pack : ListChar -> String
`  Turns a list of characters into a string.`

Totality: total
pi : Double
Totality: total
plus : Nat -> Nat -> Nat
`  Add two natural numbers.  @ x the number to case-split on  @ y the other numberpublic export`

Totality: total
pow : Double -> Double -> Double
Totality: total
rangeFrom : Rangea => a -> Streama
Totality: total
rangeFromThen : Rangea => a -> a -> Streama
Totality: total
rangeFromThenTo : Rangea => a -> a -> a -> Lista
Totality: total
rangeFromTo : Rangea => a -> a -> Lista
Totality: total
reverse : String -> String
`  Reverses the elements within a string.    ```idris example  reverse "ABC"  ```  ```idris example  reverse ""  ````

Totality: total
sin : Double -> Double
Totality: total
sinh : Double -> Double
Totality: total
sqrt : Double -> Double
Totality: total
strCons : Char -> String -> String
`  Adds a character to the front of the specified string.    ```idris example  strCons 'A' "B"  ```  ```idris example  strCons 'A' ""  ````

Totality: total
strUncons : String -> Maybe (Char, String)
Totality: total
substr : Nat -> Nat -> String -> String
`  Returns a substring of a given string    @ index The (zero based) index of the string to extract. If this is beyond  the end of the string, the function returns the empty string.  @ len The desired length of the substring. Truncated if this exceeds the  length of the input  @ subject The string to return a portion of`

Totality: total
tail : Streama -> Streama
`  All but the first element.`

Totality: total
take : Nat -> Streama -> Lista
`  Take precisely n elements from the stream.  @ n how many elements to take  @ xs the stream`

Totality: total
takeBefore : (n -> Bool) -> Streamn -> Listn
takeUntil : (n -> Bool) -> Streamn -> Listn
tan : Double -> Double
Totality: total
tanh : Double -> Double
Totality: total
toLower : Char -> Char
`  Convert a letter to the corresponding lower-case letter, if any.  Non-letters are ignored.`

Totality: total
toUpper : Char -> Char
`  Convert a letter to the corresponding upper-case letter, if any.  Non-letters are ignored.`

Totality: total
unpack : String -> ListChar
`  Turns a string into a list of characters.    ```idris example  unpack "ABC"  ````

Totality: total
whenJust : Applicativef => Maybea -> (a -> f ()) -> f ()
`  Execute an applicative expression when the Maybe is Just`

Totality: total