Stream: Coq users

Topic: Iteratively developing definitions


view this post on Zulip Callan McGill (Jan 28 2022 at 04:07):

Sometimes it is quite a pain to write direct definitions in Coq compared to writing in tactic mode as that can be done iteratively. Is there any way to do this in just gallina and if not what is considered bad style to define via tactics?

view this post on Zulip Li-yao (Jan 28 2022 at 05:19):

You can use the refine tactic to write terms with holes and see the subgoals interactively.

view this post on Zulip Callan McGill (Jan 28 2022 at 05:33):

Is it considered bad taste to write Definitions like that? Or do you re-factor after it has been worked out?

view this post on Zulip Guillaume Melquiond (Jan 28 2022 at 06:11):

I guess it is a matter of readability. If it would make it more readable to translate the definition back from tactics, I usually do.


Last updated: Feb 01 2023 at 12:30 UTC