- the : (a : Type) ->
(x : a) ->
a
Manually assign a type to an expression.
- a
the type to assign
- x
the element to get the type
- snd : (a,
b) ->
b
Return the second element of a pair.
- id : a ->
a
Identity function.
- fst : (s,
t) ->
s
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 : A) ->
Dec A
The case where the property holds
- prf
the proof
- No : (contra : A ->
Void) ->
Dec A
The case where the property holding would be a contradiction
- contra
a demonstration that A would be a contradiction
- (.) : (b ->
c) ->
(a ->
b) ->
a ->
c
Function composition
- Fixity
- Left associative, precedence 9