Zulip Chat Archive

Stream: general

Topic: -class


Reid Barton (May 24 2020 at 01:19):

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 (May 24 2020 at 01:21):

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

Johan Commelin (May 24 2020 at 03:23):

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 (May 24 2020 at 04:05):

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

Yury G. Kudryashov (May 24 2020 at 04:08):

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 (May 24 2020 at 04:10):

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


Last updated: Dec 20 2023 at 11:08 UTC