- (===) : a -> a -> Type
- Totality: total
Fixity Declaration: infix operator, level 6 - data Equal : a -> b -> Type
- Totality: total
Constructor: - Refl : x = x
- 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
- 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
- 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
- data LPair : Type -> Type -> Type
A pair type where each component is linear
Totality: total
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
- data 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
- data Unit : Type
The canonical single-element type, also known as the trivially true
proposition.
Totality: total
Constructor: - MkUnit : ()
The trivial constructor for `()`.
- 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- 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 : FromChar Char
- Totality: total
- defaultDouble : FromDouble Double
- Totality: total
- defaultString : FromString String
- Totality: total
- delay : a -> Lazy a
- Totality: total
- force : Lazy a -> a
- Totality: total
- fromChar : FromChar ty => Char -> ty
Conversion from Char.
Totality: total- fromDouble : FromDouble ty => Double -> ty
Conversion from Double.
Totality: total- fromString : FromString ty => 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 : MkDPair a pa = MkDPair b qb -> a = b
Injectivity of MkDPair (first components)
Totality: total- mkDPairInjectiveSnd : MkDPair a pa = MkDPair a qa -> pa = qa
Injectivity of MkDPair (snd components)
Totality: total- replace : {0 p : _ -> Type} -> (0 _ : x = y) -> p x -> p y
Perform substitution in a term according to some equality.
Totality: total- rewrite__impl : (0 p : (a -> Type)) -> (0 _ : x = y) -> 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- 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