Idris2Doc : Prelude.Basics

# Prelude.Basics

## Definitions

`Not : Type -> Type`
`  `Not x` is an alias for `x -> Void`, indicating that any term of type `x`  leads to a contradiction. It can be used in conjunction with `void` or  `absurd`.`

Totality: total
Visibility: public export
`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
Visibility: public export
`id : a -> a`
`  Identity function.`

Totality: total
Visibility: public export
`dup : a -> (a, a)`
`  Function that duplicates its input`

Totality: total
Visibility: public export
`const : a -> b -> a`
`  Constant function.  Ignores its second argument.`

Totality: total
Visibility: public export
`(.) : (b -> c) -> (a -> b) -> a -> c`
`  Function composition.`

Totality: total
Visibility: public export
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
Visibility: public export
Fixity Declaration: infixr operator, level 9
`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
Visibility: public export
Fixity Declaration: infixl operator, level 0
`flip : (a -> b -> c) -> b -> a -> c`
`  Takes in the first two arguments in reverse order.  @ f the function to flip`

Totality: total
Visibility: public export
`apply : (a -> b) -> a -> b`
`  Function application.`

Totality: total
Visibility: public export
`curry : ((a, b) -> c) -> a -> b -> c`
Totality: total
Visibility: public export
`uncurry : (a -> b -> c) -> (a, b) -> c`
Totality: total
Visibility: public export
`(\$) : {0 b : a -> Type} -> ((x : a) -> b x) -> (x : a) -> b x`
`  (\$) is compiled specially to shortcut any tricky unification issues, but if  it did have a type this is what it would be, and it might be useful to  use directly sometimes (e.g. in higher order functions)`

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 0
`cong : (0 f : (t -> u)) -> (0 _ : a = b) -> f a = f b`
`  Equality is a congruence.`

Totality: total
Visibility: public export
`cong2 : (0 f : (t1 -> t2 -> u)) -> (0 _ : a = b) -> (0 _ : c = d) -> f a c = f b d`
`  Two-holed congruence.`

Totality: total
Visibility: export
`depCong : {0 p : a -> Type} -> (0 f : ((x : a) -> p x)) -> x1 = x2 -> f x1 = f x2`
`  Dependent version of `cong`.`

Totality: total
Visibility: public export
`depCong2 : {0 p : a -> Type} -> {0 q : (x : a) -> p x -> Type} -> (0 f : ((x : a) -> (y : p x) -> q x y)) -> x1 = x2 -> y1 = y2 -> f x1 y1 = f x2 y2`
`  Dependent version of `cong2`.`

Totality: total
Visibility: public export
`irrelevantEq : (0 _ : a = b) -> a = b`
`  Irrelevant equalities can always be made relevant`

Totality: total
Visibility: export
`data Bool : Type`
`  Boolean Data Type.`

Totality: total
Visibility: public export
Constructors:
`False : Bool`
`True : Bool`

Hints:
`Eq Bool`
`Ord Bool`
`Show Bool`
`Uninhabited (True = False)`
`Uninhabited (False = True)`
`not : Bool -> Bool`
`  Boolean NOT.`

Totality: total
Visibility: public export
`(&&) : Bool -> Lazy Bool -> Bool`
`  Boolean AND only evaluates the second argument if the first is `True`.`

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 5
`(||) : Bool -> Lazy Bool -> Bool`
`  Boolean OR only evaluates the second argument if the first is `False`.`

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
`ifThenElse : Bool -> Lazy a -> Lazy a -> a`
`  Non-dependent if-then-else`

Totality: total
Visibility: public export
`intToBool : Int -> Bool`
Totality: total
Visibility: public export
`data List : Type -> Type`
`  Generic lists.`

Totality: total
Visibility: public export
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.`

Hints:
`Alternative List`
`Applicative List`
`Eq a => Eq (List a)`
`Foldable List`
`Functor List`
`Monad List`
`Monoid (List a)`
`Ord a => Ord (List a)`
`Semigroup (List a)`
`Show a => Show (List a)`
`Traversable List`
`data SnocList : Type -> Type`
`  Snoc lists.`

Totality: total
Visibility: public export
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.`

Hints:
`Eq a => Eq (SnocList a)`
`Ord a => Ord (SnocList a)`