- (.) : (b ->
c) ->
(a ->
b) ->
a ->
c
Function composition
- Fixity
- Left associative, precedence 9
- 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
- Not : Type ->
Type
- apply : (a ->
b) ->
a ->
b
Function application.
- cong : (a =
b) ->
f a =
f b
Equality is a congruence.
- const : a ->
b ->
a
Constant function. Ignores its second argument.
- flip : (f : a ->
b ->
c) ->
b ->
a ->
c
Takes in the first two arguments in reverse order.
- f
the function to flip
- fst : (a,
b) ->
a
Return the first element of a pair.
- id : a ->
a
Identity function.
- snd : (a,
b) ->
b
Return the second element of a pair.
- 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