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?
You can use the
refine tactic to write terms with holes and see the subgoals interactively.
Is it considered bad taste to write Definitions like that? Or do you re-factor after it has been worked out?
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