Stream: new members
Henning Dieterichs (Oct 25 2020 at 12:47):
It seems like only theorem, lemma and example can be used to state props. Is that right? Can I define an alias for a theorem? I would like to state a "proposition".
I would like to organize my work by having a main theorem, several sections each with propositions used by the theorem. These propositions are supported by several lemmas that are not really interesting.
Yury G. Kudryashov (Oct 25 2020 at 13:29):
AFAIK, in Lean 3 this requires modifications to C++ code.
Mario Carneiro (Oct 25 2020 at 14:17):
You could make a user command, but then you have the very hard problem of replicating the
Reid Barton (Oct 25 2020 at 14:27):
Does it not work to make
proposition a user command that
Mario Carneiro (Oct 25 2020 at 14:39):
Just "theorem" on its own? No, because you have to feed a complete command to the
Mario Carneiro (Oct 25 2020 at 14:40):
so you would have to parse stuff just like
def (which sounds doable) but then convert it back to a string and parse it again with
Mario Carneiro (Oct 25 2020 at 14:41):
and I'm sure there are a half dozen ways that wouldn't roundtrip
Reid Barton (Oct 25 2020 at 14:45):
Sounds like another job for the C preprocessor then :smiling_devil:
Reid Barton (Oct 25 2020 at 14:46):
More seriously, there are a bunch of other ways to document your intent, such as writing comments; so I don't think the lack of
proposition is much of a problem.
Eric Wieser (Oct 25 2020 at 16:35):
Could you use a
Last updated: May 09 2021 at 19:11 UTC