Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proving equality of classes is unexplained #11

Open
sxhya opened this issue Mar 22, 2023 · 1 comment
Open

Proving equality of classes is unexplained #11

sxhya opened this issue Mar 22, 2023 · 1 comment

Comments

@sxhya
Copy link

sxhya commented Mar 22, 2023

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
Copy link
Contributor

valis commented Mar 29, 2023

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants