Module with parameters - Githubissues

JetBrains / Arend

The Arend Proof Assistant

https://arend-lang.github.io/

Apache License 2.0

694 stars 33 forks source link

Closed ice1000 closed 4 years ago

ice1000 commented 4 years ago

And we should be able to specify some parameters to a module and \open it

valis commented 4 years ago

Classes are modules with parameters

ice1000 commented 4 years ago

But can you \open a class with members specified partially?

valis commented 4 years ago

Yes: extend it.