Idris2Doc : Prelude.Types

Prelude.Types

Definitions
data Nat : Type
  Natural numbers: unbounded, unsigned integers which can be pattern matched.

  Totality: total
  Visibility: public export
  Constructors:
  
Z : Nat
  Zero.
  
S : Nat -> Nat
  Successor.

  Hints:
  
Cast Nat String
  
Cast Nat Integer
  
Cast Nat Int
  
Cast Nat Char
  
Cast Nat Double
  
Cast Nat Bits8
  
Cast Nat Bits16
  
Cast Nat Bits32
  
Cast Nat Bits64
  
Cast Nat Int8
  
Cast Nat Int16
  
Cast Nat Int32
  
Cast Nat Int64
  
Cast String Nat
  
Cast Double Nat
  
Cast Char Nat
  
Cast Int Nat
  
Cast Integer Nat
  
Cast Bits8 Nat
  
Cast Bits16 Nat
  
Cast Bits32 Nat
  
Cast Bits64 Nat
  
Cast Int8 Nat
  
Cast Int16 Nat
  
Cast Int32 Nat
  
Cast Int64 Nat
  
Eq Nat
  
Num Nat
  
Ord Nat
  
Range Nat
  
Show Nat
integerToNat : Integer -> Nat
  Totality: total
  Visibility: public export
plus : Nat -> Nat -> Nat
  Add two natural numbers.
  @ x the number to case-split on
  @ y the other number

  Totality: total
  Visibility: public export
minus : Nat -> Nat -> Nat
  Subtract natural numbers.
  If the second number is larger than the first, return 0.

  Totality: total
  Visibility: public export
mult : Nat -> Nat -> Nat
  Multiply natural numbers.

  Totality: total
  Visibility: public export
equalNat : Nat -> Nat -> Bool
  Totality: total
  Visibility: public export
compareNat : Nat -> Nat -> Ordering
  Totality: total
  Visibility: public export
natToInteger : Nat -> Integer
  Totality: total
  Visibility: public export
count : Foldable t => (a -> Bool) -> t a -> Nat
  Counts the number of elements that satify a predicate.

  Totality: total
  Visibility: public export
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
  Visibility: public export
  Constructors:
  
Nothing : Maybe ty
  No value stored
  
Just : ty -> Maybe ty
  A value of type `ty` is stored

  Hints:
  
Alternative Maybe
  
Applicative Maybe
  
Eq a => Eq (Maybe a)
  
Foldable Maybe
  
Functor Maybe
  
Monad Maybe
  
Monoid (Maybe a)
  
Ord a => Ord (Maybe a)
  
Semigroup (Maybe a)
  
Show a => Show (Maybe a)
  
Traversable Maybe
  
Uninhabited (Nothing = Just x)
  
Uninhabited (Just x = Nothing)
maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
  Totality: total
  Visibility: public export
whenJust : Applicative f => Maybe a -> (a -> f ()) -> f ()
  Execute an applicative expression when the Maybe is Just

  Totality: total
  Visibility: public export
record (<=>) : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkEquivalence : (a -> b) -> (b -> a) -> a <=> b

  Projections:
  
.leftToRight : a <=> b -> a -> b
  
.rightToLeft : a <=> b -> b -> a

  Fixity Declaration: infix operator, level 0
.leftToRight : a <=> b -> a -> b
  Totality: total
  Visibility: public export
leftToRight : a <=> b -> a -> b
  Totality: total
  Visibility: public export
.rightToLeft : a <=> b -> b -> a
  Totality: total
  Visibility: public export
rightToLeft : a <=> b -> b -> a
  Totality: total
  Visibility: public export
data Dec : Type -> Type
  Decidability.  A decidable property either holds or is a contradiction.

  Totality: total
  Visibility: public export
  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

  Hints:
  
Uninhabited (Yes p = No q)
  
Uninhabited (No p = Yes q)
viaEquivalence : a <=> b -> Dec a -> Dec b
  Totality: total
  Visibility: public export
data Either : Type -> Type -> Type
  A sum type.

  Totality: total
  Visibility: public export
  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.

  Hints:
  
Applicative (Either e)
  
Bifoldable Either
  
Bifunctor Either
  
Bitraversable Either
  
(Eq a, Eq b) => Eq (Either a b)
  
Foldable (Either e)
  
Functor (Either e)
  
Monad (Either e)
  
(Ord a, Ord b) => Ord (Either a b)
  
(Show a, Show b) => Show (Either a b)
  
Traversable (Either e)
  
Uninhabited (Left p = Right q)
  
Uninhabited (Right p = Left q)
  
Either (Uninhabited a) (Uninhabited b) => Uninhabited (a, b)
  
Uninhabited a => Uninhabited b => Uninhabited (Either a b)
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
  Visibility: public export
(<><) : SnocList a -> List a -> SnocList a
  'fish': Action of lists on snoc-lists

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 7
(<>>) : SnocList a -> List a -> List a
  'chips': Action of snoc-lists on lists

  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 6
(++) : SnocList a -> SnocList a -> SnocList a
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
length : SnocList a -> Nat
  Totality: total
  Visibility: public export
filter : (a -> Bool) -> SnocList a -> SnocList a
  Filters a snoc-list according to a simple classifying function

  Totality: total
  Visibility: public export
mapMaybe : (a -> Maybe b) -> SnocList a -> SnocList b
  Apply a partial function to the elements of a list, keeping the ones at which
  it is defined.

  Totality: total
  Visibility: public export
reverseOnto : SnocList a -> SnocList a -> SnocList a
  Reverse the second snoclist, prepending its elements to the first.

  Totality: total
  Visibility: public export
reverse : SnocList a -> SnocList a
  Reverses the given list.

  Totality: total
  Visibility: public export
tailRecAppend : SnocList a -> SnocList a -> SnocList a
  Tail-recursive append. Uses of (++) are automatically transformed to
  this. The only reason this is exported is that the proof of equivalence
  lives in a different module.

  Totality: total
  Visibility: public export
lengthPlus : Nat -> SnocList a -> Nat
  Returns the first argument plus the length of the second.

  Totality: total
  Visibility: public export
lengthTR : SnocList a -> Nat
  `length` implementation that uses tail recursion. Exported so
  lengthTRIsLength can see it.

  Totality: total
  Visibility: public export
mapMaybeAppend : List b -> (a -> Maybe b) -> SnocList a -> SnocList b
  Utility for implementing `mapMaybeTR`

  Totality: total
  Visibility: public export
mapMaybeTR : (a -> Maybe b) -> SnocList a -> SnocList b
  Tail recursive version of `mapMaybe`. This is automatically used
  at runtime due to a `transform` rule.

  Totality: total
  Visibility: public export
filterAppend : List a -> (a -> Bool) -> SnocList a -> SnocList a
  Utility for implementing `filterTR`

  Totality: total
  Visibility: public export
filterTR : (a -> Bool) -> SnocList a -> SnocList a
  Tail recursive version of `filter`. This is automatically used
  at runtime due to a `transform` rule.

  Totality: total
  Visibility: public export
(++) : List a -> List a -> List a
  Concatenate one list with another.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
length : List a -> Nat
  Returns the length of the list.

  Totality: total
  Visibility: public export
filter : (a -> Bool) -> List a -> List a
  Applied to a predicate and a list, returns the list of those elements that
  satisfy the predicate.

  Totality: total
  Visibility: public export
mapMaybe : (a -> Maybe b) -> List a -> List b
  Apply a partial function to the elements of a list, keeping the ones at which it is defined.

  Totality: total
  Visibility: public export
reverseOnto : List a -> List a -> List a
  Reverse the second list, prepending its elements to the first.

  Totality: total
  Visibility: public export
reverse : List a -> List a
  Reverses the given list.

  Totality: total
  Visibility: public export
tailRecAppend : List a -> List a -> List a
  Tail-recursive append. Uses of (++) are automatically transformed to
  this. The only reason this is exported is that the proof of equivalence
  lives in a different module.

  Totality: total
  Visibility: public export
lengthPlus : Nat -> List a -> Nat
  Returns the first argument plus the length of the second.

  Totality: total
  Visibility: public export
lengthTR : List a -> Nat
  `length` implementation that uses tail recursion. Exported so
  lengthTRIsLength can see it.

  Totality: total
  Visibility: public export
mapImpl : (a -> b) -> List a -> List b
  Totality: total
  Visibility: public export
mapAppend : SnocList b -> (a -> b) -> List a -> List b
  Utility for implementing `mapTR`

  Totality: total
  Visibility: public export
mapTR : (a -> b) -> List a -> List b
  Tail recursive version of `map`. This is automatically used
  at runtime due to a `transform` rule.

  Totality: total
  Visibility: public export
mapMaybeAppend : SnocList b -> (a -> Maybe b) -> List a -> List b
  Utility for implementing `mapMaybeTR`

  Totality: total
  Visibility: public export
mapMaybeTR : (a -> Maybe b) -> List a -> List b
  Tail recursive version of `mapMaybe`. This is automatically used
  at runtime due to a `transform` rule.

  Totality: total
  Visibility: public export
filterAppend : SnocList a -> (a -> Bool) -> List a -> List a
  Utility for implementing `filterTR`

  Totality: total
  Visibility: public export
filterTR : (a -> Bool) -> List a -> List a
  Tail recursive version of `filter`. This is automatically used
  at runtime due to a `transform` rule.

  Totality: total
  Visibility: public export
listBindOnto : (a -> List b) -> List b -> List a -> List b
  Totality: total
  Visibility: public export
listBind : List a -> (a -> List b) -> List b
  Totality: total
  Visibility: public export
fastConcat : List String -> String
elemBy : Foldable t => (a -> a -> Bool) -> a -> t a -> Bool
  Check if something is a member of a list using a custom comparison.

  Totality: total
  Visibility: public export
elem : Foldable t => Eq a => a -> t a -> Bool
  Check if something is a member of a list using the default Boolean equality.

  Totality: total
  Visibility: public export
getAt : Nat -> List a -> Maybe a
  Lookup a value at a given position

  Totality: total
  Visibility: export
data Stream : Type -> Type
  An infinite stream.

  Totality: total
  Visibility: public export
  Constructor: 
(::) : a -> Inf (Stream a) -> Stream a

  Hint: 
Functor Stream
head : Stream a -> a
  The first element of an infinite stream.

  Totality: total
  Visibility: public export
tail : Stream a -> Stream a
  All but the first element.

  Totality: total
  Visibility: public export
take : Nat -> Stream a -> List a
  Take precisely n elements from the stream.
  @ n how many elements to take
  @ xs the stream

  Totality: total
  Visibility: public export
(++) : String -> String -> String
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
length : String -> Nat
  Returns the length of the string.
  
  ```idris example
  length ""
  ```
  ```idris example
  length "ABC"
  ```

  Totality: total
  Visibility: public export
reverse : String -> String
  Reverses the elements within a string.
  
  ```idris example
  reverse "ABC"
  ```
  ```idris example
  reverse ""
  ```

  Totality: total
  Visibility: public export
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
  Visibility: public export
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
  Visibility: public export
strUncons : String -> Maybe (Char, String)
  Totality: total
  Visibility: public export
pack : List Char -> String
  Turns a list of characters into a string.

  Totality: total
  Visibility: public export
fastPack : List Char -> String
unpack : String -> List Char
  Turns a string into a list of characters.
  
  ```idris example
  unpack "ABC"
  ```

  Totality: total
  Visibility: public export
fastUnpack : String -> List Char
isUpper : Char -> Bool
  Returns true if the character is in the range [A-Z].

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

  Totality: total
  Visibility: public export
isAlpha : Char -> Bool
  Returns true if the character is in the ranges [A-Z][a-z].

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

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

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

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

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

  Totality: total
  Visibility: public export
toLower : Char -> Char
  Convert a letter to the corresponding lower-case letter, if any.
  Non-letters are ignored.

  Totality: total
  Visibility: public export
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
  Visibility: public export
isOctDigit : Char -> Bool
  Returns true if the character is an octal digit.

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

  Totality: total
  Visibility: public export
chr : Int -> Char
  Convert the number to its backend dependent (usually Unicode) Char
  equivalent.

  Totality: total
  Visibility: public export
ord : Char -> Int
  Return the backend dependent (usually Unicode) numerical equivalent of the Char.

  Totality: total
  Visibility: public export
pi : Double
  Totality: total
  Visibility: public export
euler : Double
  Totality: total
  Visibility: public export
exp : Double -> Double
  Totality: total
  Visibility: public export
log : Double -> Double
  Totality: total
  Visibility: public export
pow : Double -> Double -> Double
  Totality: total
  Visibility: public export
sin : Double -> Double
  Totality: total
  Visibility: public export
cos : Double -> Double
  Totality: total
  Visibility: public export
tan : Double -> Double
  Totality: total
  Visibility: public export
asin : Double -> Double
  Totality: total
  Visibility: public export
acos : Double -> Double
  Totality: total
  Visibility: public export
atan : Double -> Double
  Totality: total
  Visibility: public export
sinh : Double -> Double
  Totality: total
  Visibility: public export
cosh : Double -> Double
  Totality: total
  Visibility: public export
tanh : Double -> Double
  Totality: total
  Visibility: public export
sqrt : Double -> Double
  Totality: total
  Visibility: public export
floor : Double -> Double
  Totality: total
  Visibility: public export
ceiling : Double -> Double
  Totality: total
  Visibility: public export
countFrom : n -> (n -> n) -> Stream n
  Totality: total
  Visibility: public export
takeUntil : (n -> Bool) -> Stream n -> List n
  Visibility: public export
takeBefore : (n -> Bool) -> Stream n -> List n
  Visibility: public export
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
  
Range Char
rangeFromTo : Range a => a -> a -> List a
  Totality: total
  Visibility: public export
rangeFromThenTo : Range a => a -> a -> a -> List a
  Totality: total
  Visibility: public export
rangeFrom : Range a => a -> Stream a
  Totality: total
  Visibility: public export
rangeFromThen : Range a => a -> a -> Stream a
  Totality: total
  Visibility: public export