A function returning a value in a dependent type
Define a function with a dependent type that returns
true
for natural numbers of the form
4n+1
,
false
for numbers of the form
4n+3
and
n
for numbers of the form
2n
.
Solution
This file
Going home