- data Dec : Type -> Type
Decidability. A decidable property either holds or is a contradiction.
Totality: total
Constructors:
- Yes : prop -> Dec prop
The case where the property holds.
@ prf the proof
- No : Not prop -> Dec prop
The case where the property holding would be a contradiction.
@ contra a demonstration that prop would be a contradiction
- data Either : Type -> Type -> Type
A sum type.
Totality: total
Constructors:
- Left : a -> Either a b
One possibility of the sum, conventionally used to represent errors.
- Right : b -> Either a b
The other possibility, conventionally used to represent success.
- data 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 : Maybe ty
No value stored
- Just : ty -> Maybe ty
A value of type `ty` is stored
- data Nat : Type
Natural numbers: unbounded, unsigned integers which can be pattern matched.
Totality: total
Constructors:
- Z : Nat
Zero.
- S : Nat -> Nat
Successor.
- interface Range : Type -> Type
- Parameters: a
Constructor: MkRange
Methods:
- rangeFromTo : a -> a -> List a
- rangeFromThenTo : a -> a -> a -> List a
- rangeFrom : a -> Stream a
- rangeFromThen : a -> a -> Stream a
Implementations:
- Range Nat
- (Integral a, (Ord a, Neg a)) => Range a
- 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 : Foldable t => (a -> Bool) -> t a -> Nat
Counts the number of elements that satify a predicate.
Totality: total- countFrom : n -> (n -> n) -> Stream n
- Totality: total
- either : Lazy (a -> c) -> Lazy (b -> c) -> Either a b -> 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 : Eq a => a -> List a -> 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 : List String -> String
- fastPack : List Char -> String
- fastUnpack : String -> List Char
- floor : Double -> Double
- Totality: total
- getAt : Nat -> List a -> Maybe a
Lookup a value at a given position
Totality: total- head : Stream a -> 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) -> Maybe a -> 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 : Range a => a -> Stream a
- Totality: total
- rangeFromThen : Range a => a -> a -> Stream a
- Totality: total
- rangeFromThenTo : Range a => a -> a -> a -> List a
- Totality: total
- rangeFromTo : Range a => a -> a -> List a
- 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 : Stream a -> Stream a
All but the first element.
Totality: total- take : Nat -> Stream a -> List a
Take precisely n elements from the stream.
@ n how many elements to take
@ xs the stream
Totality: total- takeBefore : (n -> Bool) -> Stream n -> List n
-
- takeUntil : (n -> Bool) -> Stream n -> List n
-
- 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- whenJust : Applicative f => Maybe a -> (a -> f ()) -> f ()
Execute an applicative expression when the Maybe is Just
Totality: total