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
dataUnit : 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 ()
dataPair : 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:
Monoida=>Applicative (Paira)
BifoldablePair
BifunctorPair
BitraversablePair
(Eqa, Eqb) =>Eq (Eitherab)
Eqa=>Eqb=>Eq (a, b)
Foldable (Paira)
Functor (Paira)
Monoida=>Monad (Paira)
Monoida=>Monoidb=>Monoid (a, b)
(Orda, Ordb) =>Ord (Eitherab)
Orda=>Ordb=>Ord (a, b)
(Integrala, (Orda, Nega)) =>Rangea
Semigroupa=>Semigroupb=>Semigroup (a, b)
(Showa, Showb) =>Show (a, b)
(Showa, Show (py)) =>Show (DPairap)
(Showa, Showb) =>Show (Eitherab)
Traversable (Paira)
Either (Uninhabiteda) (Uninhabitedb) =>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
dataLPair : Type->Type->Type
  A pair type where each component is linear

Totality: total
Visibility: public export
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
recordDPair : (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) ->pfst->DPairap

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

Hint: 
(Showa, Show (py)) =>Show (DPairap)
.fst : DPairap->a
Totality: total
Visibility: public export
fst : DPairap->a
Totality: total
Visibility: public export
.snd : ({rec:0} : DPairap) ->p (fst{rec:0})
Totality: total
Visibility: public export
snd : ({rec:0} : DPairap) ->p (fst{rec:0})
Totality: total
Visibility: public export
dataRes : (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_ : tval) ->Resat
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
Visibility: public export
Hints:
EqVoid
InterpolationVoid
OrdVoid
ShowVoid
UninhabitedVoid
dataEqual : 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 : (0p : (a->Type)) -> (0_ : x=y) -> (1_ : 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
Visibility: public export
replace : {0p : {_:423}->Type} -> (0_ : x=y) -> (1_ : px) ->py
  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
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
fromString : FromStringty=>String->ty
  Conversion from String.

Totality: total
Visibility: public export
defaultString : FromStringString
Totality: total
Visibility: public export
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
fromChar : FromCharty=>Char->ty
  Conversion from Char.

Totality: total
Visibility: public export
defaultChar : FromCharChar
Totality: total
Visibility: public export
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
fromDouble : FromDoublety=>Double->ty
  Conversion from Double.

Totality: total
Visibility: public export
defaultDouble : FromDoubleDouble
Totality: total
Visibility: public export