- ($) : {0 b : a -> Type} -> ((x : a) -> b x) -> (x : a) -> b x
- 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- data Bool : Type
Boolean Data Type.
Totality: total
Constructors:
- False : Bool
- True : Bool
- data List : Type -> Type
Generic lists.
Totality: total
Constructors:
- Nil : List a
Empty list
- (::) : a -> List a -> List a
A non-empty list, consisting of a head element and the rest of the list.
- Not : Type -> Type
- Totality: total
- data SnocList : Type -> Type
Snoc lists.
Totality: total
Constructors:
- Lin : SnocList a
Empty snoc-list
- (:<) : SnocList a -> a -> SnocList a
A non-empty snoc-list, consisting of the rest of the snoc-list and the final element.
- apply : (a -> b) -> a -> b
Function application.
Totality: total- cong : (0 f : (t -> u)) -> a = b -> f a = f b
Equality is a congruence.
Totality: total- cong2 : (0 f : (t1 -> t2 -> u)) -> a = b -> c = d -> f a c = f b d
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