Loading collection data...
Collections are a way for you to organize kata so that you can create your own training routines. Every collection you create is public and automatically sharable with other warriors. After you have added a few kata to a collection you and others can train on the kata contained within the collection.
Get started now by creating a new collection.
This comment is hidden because it contains spoiler information about the solution
Hmm, I assume then it has to do with kinds and why dependently typed languages exist for actual proofs, but take anything I write with a grain of salt as I'm also learning haskell and mostly speculate.
This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
If I understand correctly, the
eq
function is only partially defined on the cases whena
andb
are actually equal.How is it legit to use
eq
in a more general case as ineq (plus a b) (plus b a)
?Thanks for the hint, it's very helpful. I was finally able to finish this Kata.
I personally think the description on this particular proposition is a bit confusing, at least to me. In the beginning I didn't even know I'm suppose implement this function at all. Perhaps we can add a little bit more elaboration on how this is supposed to be done and add a placeholder on the implementation indicating this is meant to be completed by the reader.
Anyway it's a very interesting Kata, thank you and lolisa for your work :p
You missed one very obvious case. Don't forget that it's a
Maybe a -> Maybe b
, nota -> Maybe b
;-)It's not an issue, a question ;-)
Hi folks. I'm playing with this Kata and have no idea how to implement the false proposition:
It cannot be proven, which is obvious: if we get
Nothing
by feedingJust a
to theMaybe a -> Maybe b
part of the isomorphism, we have no way to retrieve ab
.Leaving
isoUnMaybe = undefined
doesn't seem to pass the final tests. Neither does this work:The error says it panicked by calling
fromJust
onNothing
. Perhaps I should return some specific error message?