-class

Stream: general

[Reid Barton]

rss-bot said:

feat(library/class): support local attribute [-instance] (#240)
feat(library/class): support local attribute [-instance] (#240)

Fixes #27.
https://github.com/leanprover-community/lean/commit/a1bf3fd63336d28697a1e0a69f5753b913f3b39a

Would it be easy to support local attribute [-class]? Classes are way too hard for me.

[Reid Barton]

I guess it wouldn't accomplish what I really want, namely, turning [] parameters back into () parameters

[Johan Commelin]

In coq you can change the sort of variables after the definition, from () to {} etc... it would be nice to occasionally do that

[Mario Carneiro]

Well you can, with a type ascription, but this is more verbose than just using @foo _ _ _ _

[Yury G. Kudryashov]

I think that Johan was talking about something like Coq https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#coq:cmd.arguments-implicits

[Yury G. Kudryashov]

I think that global version is a bad idea but I'd love to have local arguments