tutorial-code
tutorial-code copied to clipboard
Proving equality of classes is unexplained
To be able show that the StateMonad
is a monad, you need to be able to prove equality of two instances of classes. Even I only know that this can be done using tactic ext
and don't how this can be done in Arend w/o tactics. Add more hints to the exercise.
It can be done quite easily without tactics or anything that was not explained at this point.