Idris2Doc : Builtin

Builtin

(===) : a -> a -> Type

Fixity Declaration: infix operator, level 6
Equal : a -> b -> Type
Totality: total
Constructor: 
Refl : x = x
FromString : Type -> Type
Interface for types that can be constructed from string literals.
Parameters: ty
Methods:
fromString : String -> ty
Conversion from String.

Implementation: 
FromString String
LPair : Type -> Type -> Type
A pair type where each component is linear
Totality: total
Constructor: 
(#) : (1 _ : a) -> (1 _ : b) -> LPairab
Pair : Type -> Type -> Type
The non-dependent pair type, also known as conjunction.
Totality: total
Constructor: 
MkPair : a -> b -> (a, b)
A pair of elements.
@ a the left element of the pair
@ b the right element of the pair
Unit : Type
The canonical single-element type, also known as the trivially true
proposition.
Totality: total
Constructor: 
MkUnit : Unit
The trivial constructor for `()`.
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
assert_linear : (1 _ : (a -> b)) -> (1 _ : a) -> b
Assert to the usage checker that the given function uses its argument linearly.
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)
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.
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!
defaultString : FromString String
delay : a -> Lazy a
force : Lazy a -> a
fromString : FromStringty => String -> ty
Conversion from String.
fst : (a, b) -> a
Return the first element of a pair.
idris_crash : String -> a
mkDPairInjectiveFst : MkDPairapa = MkDPairbqb -> a = b
Injectivity of MkDPair (first components)
mkDPairInjectiveSnd : MkDPairapa = MkDPairaqa -> pa = qa
Injectivity of MkDPair (snd components)
replace : {0 p : {_:161} -> Type} -> (0 _ : x = y) -> px -> py
Perform substitution in a term according to some equality.
rewrite__impl : (0 p : (a -> Type)) -> (0 _ : x = y) -> py -> px
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.
snd : (a, b) -> b
Return the second element of a pair.
sym : (0 _ : x = y) -> y = x
Symmetry of propositional equality.
trans : (0 _ : a = b) -> (0 _ : b = c) -> a = c
Transitivity of propositional equality.
(~=~) : 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

Fixity Declaration: infix operator, level 6