Idris2Doc : Builtin

Builtin

(===) : a -> a -> Type
Totality: total
Fixity Declaration: infix operator, level 6
dataEqual : a -> b -> Type
Totality: total
Constructor: 
Refl : x = x
interfaceFromChar : Type -> Type
  Interface for types that can be constructed from char literals.

Parameters: ty
Constructor: MkFromChar
Methods:
fromChar : Char -> ty
  Conversion from Char.

Implementation: 
FromCharChar
interfaceFromDouble : Type -> Type
  Interface for types that can be constructed from double literals.

Parameters: ty
Constructor: MkFromDouble
Methods:
fromDouble : Double -> ty
  Conversion from Double.

Implementation: 
FromDoubleDouble
interfaceFromString : Type -> Type
  Interface for types that can be constructed from string literals.

Parameters: ty
Constructor: MkFromString
Methods:
fromString : String -> ty
  Conversion from String.

Implementation: 
FromStringString
dataLPair : Type -> Type -> Type
  A pair type where each component is linear

Totality: total
Constructor: 
(#) : (1 _ : a) -> (1 _ : b) -> LPairab
  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
dataPair : 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
dataUnit : Type
  The canonical single-element type, also known as the trivially true
proposition.

Totality: total
Constructor: 
MkUnit : ()
  The trivial constructor for `()`.
dataVoid : 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.

Totality: total
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
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
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
defaultChar : FromCharChar
Totality: total
defaultDouble : FromDoubleDouble
Totality: total
defaultString : FromStringString
Totality: total
delay : a -> Lazy a
Totality: total
force : Lazy a -> a
Totality: total
fromChar : FromCharty => Char -> ty
  Conversion from Char.

Totality: total
fromDouble : FromDoublety => Double -> ty
  Conversion from Double.

Totality: total
fromString : FromStringty => String -> ty
  Conversion from String.

Totality: total
fst : (a, b) -> a
  Return the first element of a pair.

Totality: total
idris_crash : String -> a
mkDPairInjectiveFst : MkDPairapa = MkDPairbqb -> a = b
  Injectivity of MkDPair (first components)

Totality: total
mkDPairInjectiveSnd : MkDPairapa = MkDPairaqa -> pa = qa
  Injectivity of MkDPair (snd components)

Totality: total
replace : {0 p : _ -> Type} -> (0 _ : x = y) -> px -> py
  Perform substitution in a term according to some equality.

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

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

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

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

Totality: total
(~=~) : 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
Fixity Declaration: infix operator, level 6