Zulip Chat Archive
Stream: lean4
Topic: how to def even
BANGJI HU (Jul 04 2024 at 14:24):
Ira Fesefeldt (Jul 04 2024 at 14:48):
If you want help with your problem, its wise to
- Explain your problem or question
- Post your code surrounded by three backticks like \``` this \``` without \ producing
thisinstead of as a file.
Yury G. Kudryashov (Jul 04 2024 at 14:53):
See #mwe
Yury G. Kudryashov (Jul 04 2024 at 14:55):
And src#Even
Last updated: May 02 2025 at 03:31 UTC