Idris2Doc : Builtin

# Builtin

## Definitions

`assert_total : (1 _ : a) -> a`
`  Assert to the totality checker that the given expression will always  terminate.    The multiplicity of its argument is 1, so `assert_total` won't affect how  many times variables are used. If you're not writing a linear function,  this doesn't make a difference.    Note: assert_total can reduce at compile time, if required for unification,  which might mean that it's no longer guarded a subexpression. Therefore,  it is best to use it around the smallest possible subexpression.`

Totality: total
Visibility: public export
`assert_smaller : (0 _ : a) -> (1 _ : b) -> b`
`  Assert to the totality checker that y is always structurally smaller than x  (which is typically a pattern argument, and *must* be in normal form for  this to work).    The multiplicity of x is 0, so in a linear function, you can pass values to  x even if they have already been used.  The multiplicity of y is 1, so `assert_smaller` won't affect how many times  its y argument is used.  If you're not writing a linear function, the multiplicities don't make a  difference.    @ x the larger value (typically a pattern argument)  @ y the smaller value (typically an argument to a recursive call)`

Totality: total
Visibility: public export
`data Unit : Type`
`  The canonical single-element type, also known as the trivially true  proposition.`

Totality: total
Visibility: public export
Constructor:
`MkUnit : ()`
`  The trivial constructor for `()`.`

Hints:
`Eq ()`
`Monoid ()`
`Ord ()`
`Semigroup ()`
`Show ()`
`data Pair : Type -> Type -> Type`
`  The non-dependent pair type, also known as conjunction.`

Totality: total
Visibility: public export
Constructor:
`MkPair : a -> b -> (a, b)`
`  A pair of elements.  @ a the left element of the pair  @ b the right element of the pair`

Hints:
`Monoid a => Applicative (Pair a)`
`Bifoldable Pair`
`Bifunctor Pair`
`Bitraversable Pair`
`(Eq a, Eq b) => Eq (Either a b)`
`Eq a => Eq b => Eq (a, b)`
`Foldable (Pair a)`
`Functor (Pair a)`
`Monoid a => Monad (Pair a)`
`Monoid a => Monoid b => Monoid (a, b)`
`(Ord a, Ord b) => Ord (Either a b)`
`Ord a => Ord b => Ord (a, b)`
`(Integral a, (Ord a, Neg a)) => Range a`
`Semigroup a => Semigroup b => Semigroup (a, b)`
`(Show a, Show b) => Show (a, b)`
`(Show a, Show (p y)) => Show (DPair a p)`
`(Show a, Show b) => Show (Either a b)`
`Traversable (Pair a)`
`Either (Uninhabited a) (Uninhabited b) => Uninhabited (a, b)`
`fst : (a, b) -> a`
`  Return the first element of a pair.`

Totality: total
Visibility: public export
`snd : (a, b) -> b`
`  Return the second element of a pair.`

Totality: total
Visibility: public export
`swap : (a, b) -> (b, a)`
`  Swap the elements in a pair`

Totality: total
Visibility: public export
`data LPair : Type -> Type -> Type`
`  A pair type where each component is linear`

Totality: total
Visibility: public export
Constructor:
`(#) : (1 _ : a) -> (1 _ : b) -> LPair a b`
`  A linear pair of elements.  If you take one copy of the linear pair apart  then you only get one copy of its left and right elements.  @ a the left element of the pair  @ b the right element of the pair`
`record DPair : (a : Type) -> (a -> Type) -> Type`
`  Dependent pairs aid in the construction of dependent types by providing  evidence that some value resides in the type.    Formally, speaking, dependent pairs represent existential quantification -  they consist of a witness for the existential claim and a proof that the  property holds for it.    @ a the value to place in the type.  @ p the dependent type that requires the value.`

Totality: total
Visibility: public export
Constructor:
`MkDPair : (fst : a) -> p fst -> DPair a p`

Projections:
`.fst : DPair a p -> a`
`.snd : ({rec:0} : DPair a p) -> p (fst {rec:0})`

Hint:
`(Show a, Show (p y)) => Show (DPair a p)`
`.fst : DPair a p -> a`
Totality: total
Visibility: public export
`fst : DPair a p -> a`
Totality: total
Visibility: public export
`.snd : ({rec:0} : DPair a p) -> p (fst {rec:0})`
Totality: total
Visibility: public export
`snd : ({rec:0} : DPair a p) -> p (fst {rec:0})`
Totality: total
Visibility: public export
`data Res : (a : Type) -> (a -> Type) -> Type`
`  A dependent variant of LPair, pairing a result value with a resource  that depends on the result value`

Totality: total
Visibility: public export
Constructor:
`(#) : (val : a) -> (1 _ : t val) -> Res a t`
`data Void : Type`
`  The empty type, also known as the trivially false proposition.    Use `void` or `absurd` to prove anything if you have a variable of type  `Void` in scope.`

Totality: total
Visibility: public export
Hints:
`Eq Void`
`Interpolation Void`
`Ord Void`
`Show Void`
`Uninhabited Void`
`data Equal : a -> b -> Type`
Totality: total
Visibility: public export
Constructor:
`Refl : x = x`
`(===) : a -> a -> Type`
Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6
`(~=~) : a -> b -> Type`
`  Explicit heterogeneous ("John Major") equality.  Use this when Idris  incorrectly chooses homogeneous equality for `(=)`.  @ a the type of the left side  @ b the type of the right side  @ x the left side  @ y the right side`

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6
`rewrite__impl : (0 p : (a -> Type)) -> (0 _ : x = y) -> (1 _ : p y) -> p x`
`  Perform substitution in a term according to some equality.    Like `replace`, but with an explicit predicate, and applying the rewrite in  the other direction, which puts it in a form usable by the `rewrite` tactic  and term.`

Totality: total
Visibility: public export
`replace : {0 p : {_:423} -> Type} -> (0 _ : x = y) -> (1 _ : p x) -> p y`
`  Perform substitution in a term according to some equality.`

Totality: total
Visibility: public export
`sym : (0 _ : x = y) -> y = x`
`  Symmetry of propositional equality.`

Totality: total
Visibility: public export
`trans : (0 _ : a = b) -> (0 _ : b = c) -> a = c`
`  Transitivity of propositional equality.`

Totality: total
Visibility: public export
`mkDPairInjectiveFst : (a ** pa) = (b ** qb) -> a = b`
`  Injectivity of MkDPair (first components)`

Totality: total
Visibility: export
`mkDPairInjectiveSnd : (a ** pa) = (a ** qa) -> pa = qa`
`  Injectivity of MkDPair (snd components)`

Totality: total
Visibility: export
`believe_me : a -> b`
`  Subvert the type checker.  This function is abstract, so it will not reduce  in the type checker.  Use it with care - it can result in segfaults or  worse!`

Totality: total
Visibility: public export
`assert_linear : (1 _ : (a -> b)) -> (1 _ : a) -> b`
`  Assert to the usage checker that the given function uses its argument linearly.`

Totality: total
Visibility: public export
`idris_crash : String -> a`
Visibility: export
`delay : a -> Lazy a`
Totality: total
Visibility: public export
`force : Lazy a -> a`
Totality: total
Visibility: public export
`interface FromString : Type -> Type`
`  Interface for types that can be constructed from string literals.`

Parameters: ty
Constructor:
`MkFromString`

Methods:
`fromString : String -> ty`
`  Conversion from String.`

Implementation:
`FromString String`
`fromString : FromString ty => String -> ty`
`  Conversion from String.`

Totality: total
Visibility: public export
`defaultString : FromString String`
Totality: total
Visibility: public export
`interface FromChar : Type -> Type`
`  Interface for types that can be constructed from char literals.`

Parameters: ty
Constructor:
`MkFromChar`

Methods:
`fromChar : Char -> ty`
`  Conversion from Char.`

Implementation:
`FromChar Char`
`fromChar : FromChar ty => Char -> ty`
`  Conversion from Char.`

Totality: total
Visibility: public export
`defaultChar : FromChar Char`
Totality: total
Visibility: public export
`interface FromDouble : Type -> Type`
`  Interface for types that can be constructed from double literals.`

Parameters: ty
Constructor:
`MkFromDouble`

Methods:
`fromDouble : Double -> ty`
`  Conversion from Double.`

Implementation:
`FromDouble Double`
`fromDouble : FromDouble ty => Double -> ty`
`  Conversion from Double.`

Totality: total
Visibility: public export
`defaultDouble : FromDouble Double`
Totality: total
Visibility: public export