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 exportassert_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 exportdata 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 exportsnd : (a, b) -> b
Return the second element of a pair.
Totality: total
Visibility: public exportswap : (a, b) -> (b, a)
Swap the elements in a pair
Totality: total
Visibility: public exportdata 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 6rewrite__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 exportreplace : {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 exportsym : (0 _ : x = y) -> y = x
Symmetry of propositional equality.
Totality: total
Visibility: public exporttrans : (0 _ : a = b) -> (0 _ : b = c) -> a = c
Transitivity of propositional equality.
Totality: total
Visibility: public exportmkDPairInjectiveFst : (a ** pa) = (b ** qb) -> a = b
Injectivity of MkDPair (first components)
Totality: total
Visibility: exportmkDPairInjectiveSnd : (a ** pa) = (a ** qa) -> pa = qa
Injectivity of MkDPair (snd components)
Totality: total
Visibility: exportbelieve_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 exportassert_linear : (1 _ : (a -> b)) -> (1 _ : a) -> b
Assert to the usage checker that the given function uses its argument linearly.
Totality: total
Visibility: public exportidris_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 exportdefaultString : 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 exportdefaultChar : 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 exportdefaultDouble : FromDouble Double
- Totality: total
Visibility: public export