Stream: Coq users

Topic: automation and proof reusability


view this post on Zulip Patrick Nicodemus (Jan 18 2022 at 02:49):

I am trying to get better at learning how to write good Ltac, proof engineering, automation, etc. i have some fairly routine things i'm working on that i expect to be highly automatable, is it considered a good use of this forum to post block quotes of code and ask for general feedback on how it could be written or rewritten or automated or made more maintainable etc.

view this post on Zulip Patrick Nicodemus (Jan 18 2022 at 02:56):

(deleted)

view this post on Zulip Patrick Nicodemus (Jan 18 2022 at 02:57):

(deleted)

view this post on Zulip Patrick Nicodemus (Jan 18 2022 at 03:36):

or just code review

view this post on Zulip Karl Palmskog (Jan 18 2022 at 07:22):

for small chunks of code (think 5-20 lines), you might get some feedback here. For larger chunks of code, we generally recommend using the Discourse forum: https://coq.discourse.group


Last updated: Jan 28 2023 at 05:02 UTC