Idris2Doc : Prelude.Basics

Prelude.Basics

($) : {0 b : a -> Type} -> ((x : a) -> bx) -> (x : a) -> bx
Totality: total
Fixity Declaration: infixr operator, level 0
(&&) : Bool -> Lazy Bool -> Bool
Boolean AND only evaluates the second argument if the first is `True`.
Totality: total
Fixity Declaration: infixr operator, level 5
(.) : (b -> c) -> (a -> b) -> a -> c
Function composition.
Totality: total
Fixity Declaration: infixr operator, level 9
(.:) : (c -> d) -> (a -> b -> c) -> a -> b -> d
Composition of a two-argument function with a single-argument one.
`(.:)` is like `(.)` but the second argument and the result are two-argument functions.
This operator is also known as "blackbird operator".
Totality: total
Fixity Declaration: infixr operator, level 9
Bool : Type
Boolean Data Type.
Totality: total
Constructors:
True : Bool
False : Bool
Not : Type -> Type
Totality: total
apply : (a -> b) -> a -> b
Function application.
Totality: total
cong : (0 f : (t -> u)) -> a = b -> fa = fb
Equality is a congruence.
Totality: total
cong2 : (0 f : (t1 -> t2 -> u)) -> a = b -> c = d -> fac = fbd
Two-holed congruence.
Totality: total
const : a -> b -> a
Constant function. Ignores its second argument.
Totality: total
curry : ((a, b) -> c) -> a -> b -> c
Totality: total
dup : a -> (a, a)
Function that duplicates its input
Totality: total
flip : (a -> b -> c) -> b -> a -> c
Takes in the first two arguments in reverse order.
@ f the function to flip
Totality: total
id : a -> a
Identity function.
Totality: total
ifThenElse : Bool -> Lazy a -> Lazy a -> a
Non-dependent if-then-else
Totality: total
intToBool : Int -> Bool
Totality: total
irrelevantEq : (0 _ : a = b) -> a = b
Irrelevant equalities can always be made relevant
Totality: total
not : Bool -> Bool
Boolean NOT.
Totality: total
on : (b -> b -> c) -> (a -> b) -> a -> a -> c
`on b u x y` runs the binary function b on the results of applying
unary function u to two arguments x and y. From the opposite perspective,
it transforms two inputs and combines the outputs.

```idris example
((+) `on` f) x y = f x + f y
```

Typical usage:

```idris example
sortBy (compare `on` fst).
```
Totality: total
Fixity Declaration: infixl operator, level 0
the : (0 a : Type) -> a -> a
Manually assign a type to an expression.
@ a the type to assign
@ x the element to get the type
Totality: total
uncurry : (a -> b -> c) -> (a, b) -> c
Totality: total
(||) : Bool -> Lazy Bool -> Bool
Boolean OR only evaluates the second argument if the first is `False`.
Totality: total
Fixity Declaration: infixr operator, level 4