arend-lang / tutorial-code

Source code & exercises in Arend's documentation
https://arend-lang.github.io/documentation/tutorial
Apache License 2.0
21 stars 9 forks source link

Proving equality of classes is unexplained #11

Open sxhya opened 1 year ago

sxhya commented 1 year ago

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.

valis commented 1 year ago

It can be done quite easily without tactics or anything that was not explained at this point.