Callan McGill (Jan 28 2022 at 04:07): 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?
Li-yao (Jan 28 2022 at 05:19):You can use the refine tactic to write terms with holes and see the subgoals interactively.
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?
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: Oct 03 2023 at 20:01 UTC