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
dataBool : Type
`  Boolean Data Type.`

Totality: total
Constructors:
False : Bool
True : Bool
dataList : Type -> Type
`  Generic lists.`

Totality: total
Constructors:
Nil : Lista
`  Empty list`
(::) : a -> Lista -> Lista
`  A non-empty list, consisting of a head element and the rest of the list.`
Not : Type -> Type
Totality: total
dataSnocList : Type -> Type
`  Snoc lists.`

Totality: total
Constructors:
Lin : SnocLista
`  Empty snoc-list`
(:<) : SnocLista -> a -> SnocLista
`  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 -> 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