IdrisDoc: Prelude.Basics

Prelude.Basics

the : (a : Type) -> (value : a) -> a

Manually assign a type to an expression.

a

the type to assign

value

the element to get the type

snd : (a, b) -> b

Return the second element of a pair.

id : a -> a

Identity function.

fst : (a, b) -> a

Return the first element of a pair.

flip : (f : a -> b -> c) -> b -> a -> c

Takes in the first two arguments in reverse order.

f

the function to flip

const : a -> b -> a

Constant function. Ignores its second argument.

cong : (a = b) -> f a = f b

Equality is a congruence.

apply : (a -> b) -> a -> b

Function application.

Not : Type -> Type
data Dec : Type -> Type

Decidability. A decidable property either holds or is a contradiction.

Yes : (prf : prop) -> Dec prop

The case where the property holds

prf

the proof

No : (contra : prop -> Void) -> Dec prop

The case where the property holding would be a contradiction

contra

a demonstration that prop would be a contradiction

(.) : (b -> c) -> (a -> b) -> a -> c

Function composition

Fixity
Left associative, precedence 9