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