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 : (0a : 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
($) : {0b : a->Type} -> ((x : a) ->bx) -> (x : a) ->bx
  ($) 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 : (0f : (t->u)) -> (0_ : a=b) ->fa=fb
  Equality is a congruence.

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

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

Totality: total
Visibility: public export
depCong2 : {0p : a->Type} -> {0q : (x : a) ->px->Type} -> (0f : ((x : a) -> (y : px) ->qxy)) ->x1=x2->y1=y2->fx1y1=fx2y2
  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
dataBool : Type
  Boolean Data Type.

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

Hints:
EqBool
OrdBool
ShowBool
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
dataList : Type->Type
  Generic lists.

Totality: total
Visibility: public export
Constructors:
Nil : Lista
  Empty list
(::) : a->Lista->Lista
  A non-empty list, consisting of a head element and the rest of the list.

Hints:
AlternativeList
ApplicativeList
Eqa=>Eq (Lista)
FoldableList
FunctorList
MonadList
Monoid (Lista)
Orda=>Ord (Lista)
Semigroup (Lista)
Showa=>Show (Lista)
TraversableList
dataSnocList : Type->Type
  Snoc lists.

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

Hints:
Eqa=>Eq (SnocLista)
Orda=>Ord (SnocLista)