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) -> (1 _ : 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

(|>) : a -> (a -> b) -> b

  Pipeline style function application, useful for chaining
  functions into a series of transformations, reading top
  to bottom.
  
  ```idris example
  [[1], [2], [3]] |> join |> map (* 2)
  ```

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 0

(<|) : (a -> b) -> a -> b

  Backwards pipeline style function application, similar to $.
  
  ```idris example
  unpack <| "hello" ++ "world"
  ```

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)