Idris2Doc : Prelude.Types

Prelude.Types

dataDec : 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 : 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
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 : 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