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