Idris2Doc : Prelude.Types

Prelude.Types

Dec : Type -> Type
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 : (prop -> Void) -> Decprop
The case where the property holding would be a contradiction.
@ contra a demonstration that prop would be a contradiction
Either : 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.
List : Type -> Type
Generic lists.
Totality: total
Constructors:
Nil : Lista
Empty list
(::) : a -> Lista -> Lista
A non-empty list, consisting of a head element and the rest of the list.
Maybe : 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
Nat : Type
Natural numbers: unbounded, unsigned integers which can be pattern matched.
Totality: total
Constructors:
Z : Nat
Zero.
S : Nat -> Nat
Successor.
Range : Type -> Type
Parameters: a
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
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
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
euler : Double
Totality: total
exp : Double -> Double
Totality: total
fastConcat : List String -> String
fastPack : List Char -> String
fastUnpack : String -> List Char
floor : Double -> Double
Totality: total
getAt : Nat -> Lista -> Maybea
Lookup a value at a given position
Totality: total
head : Streama -> a
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 : List Char -> 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
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 -> List Char
Turns a string into a list of characters.

```idris example
unpack "ABC"
```
Totality: total