Idris2Doc : Prelude.Types

Prelude.Types

Definitions

dataNat : 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:
CastNatString
CastNatInteger
CastNatInt
CastNatChar
CastNatDouble
CastNatBits8
CastNatBits16
CastNatBits32
CastNatBits64
CastNatInt8
CastNatInt16
CastNatInt32
CastNatInt64
CastStringNat
CastDoubleNat
CastCharNat
CastIntNat
CastIntegerNat
CastBits8Nat
CastBits16Nat
CastBits32Nat
CastBits64Nat
CastInt8Nat
CastInt16Nat
CastInt32Nat
CastInt64Nat
EqNat
NumNat
OrdNat
RangeNat
ShowNat
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 : Foldablet=> (a->Bool) ->ta->Nat
  Counts the number of elements that satify a predicate.

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

Hints:
AlternativeMaybe
ApplicativeMaybe
Eqa=>Eq (Maybea)
FoldableMaybe
FunctorMaybe
MonadMaybe
Monoid (Maybea)
Orda=>Ord (Maybea)
Semigroup (Maybea)
Showa=>Show (Maybea)
TraversableMaybe
Uninhabited (Nothing=Justx)
Uninhabited (Justx=Nothing)
maybe : Lazy b-> Lazy (a->b) ->Maybea->b
Totality: total
Visibility: public export
whenJust : Applicativef=>Maybea-> (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
dataDec : Type->Type
  Decidability.  A decidable property either holds or is a contradiction.

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

Hints:
Uninhabited (Yesp=Noq)
Uninhabited (Nop=Yesq)
viaEquivalence : a<=>b->Deca->Decb
Totality: total
Visibility: public export
dataEither : Type->Type->Type
  A sum type.

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

Hints:
Applicative (Eithere)
BifoldableEither
BifunctorEither
BitraversableEither
(Eqa, Eqb) =>Eq (Eitherab)
Foldable (Eithere)
Functor (Eithere)
Monad (Eithere)
(Orda, Ordb) =>Ord (Eitherab)
(Showa, Showb) =>Show (Eitherab)
Traversable (Eithere)
Uninhabited (Leftp=Rightq)
Uninhabited (Rightp=Leftq)
Either (Uninhabiteda) (Uninhabitedb) =>Uninhabited (a, b)
Uninhabiteda=>Uninhabitedb=>Uninhabited (Eitherab)
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
Visibility: public export
(<><) : SnocLista->Lista->SnocLista
  'fish': Action of lists on snoc-lists

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

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

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

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

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

Totality: total
Visibility: public export
tailRecAppend : SnocLista->SnocLista->SnocLista
  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->SnocLista->Nat
  Returns the first argument plus the length of the second.

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

Totality: total
Visibility: public export
mapMaybeAppend : Listb-> (a->Maybeb) ->SnocLista->SnocListb
  Utility for implementing `mapMaybeTR`

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

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

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

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

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

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

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

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

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

Totality: total
Visibility: public export
tailRecAppend : Lista->Lista->Lista
  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->Lista->Nat
  Returns the first argument plus the length of the second.

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

Totality: total
Visibility: public export
mapImpl : (a->b) ->Lista->Listb
Totality: total
Visibility: public export
mapAppend : SnocListb-> (a->b) ->Lista->Listb
  Utility for implementing `mapTR`

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

Totality: total
Visibility: public export
mapMaybeAppend : SnocListb-> (a->Maybeb) ->Lista->Listb
  Utility for implementing `mapMaybeTR`

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

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

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

Totality: total
Visibility: public export
listBindOnto : (a->Listb) ->Listb->Lista->Listb
Totality: total
Visibility: public export
listBind : Lista-> (a->Listb) ->Listb
Totality: total
Visibility: public export
fastConcat : ListString->String
elemBy : Foldablet=> (a->a->Bool) ->a->ta->Bool
  Check if something is a member of a list using a custom comparison.

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

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

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

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

Hint: 
FunctorStream
head : Streama->a
  The first element of an infinite stream.

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

Totality: total
Visibility: public export
take : Nat->Streama->Lista
  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 : ListChar->String
  Turns a list of characters into a string.

Totality: total
Visibility: public export
fastPack : ListChar->String
unpack : String->ListChar
  Turns a string into a list of characters.

```idris example
unpack "ABC"
```

Totality: total
Visibility: public export
fastUnpack : String->ListChar
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) ->Streamn
Totality: total
Visibility: public export
takeUntil : (n->Bool) ->Streamn->Listn
Visibility: public export
takeBefore : (n->Bool) ->Streamn->Listn
Visibility: public export
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
RangeChar
rangeFromTo : Rangea=>a->a->Lista
Totality: total
Visibility: public export
rangeFromThenTo : Rangea=>a->a->a->Lista
Totality: total
Visibility: public export
rangeFrom : Rangea=>a->Streama
Totality: total
Visibility: public export
rangeFromThen : Rangea=>a->a->Streama
Totality: total
Visibility: public export