Guillaume Melquiond (Mar 11 2021 at 12:26): Guillaume Melquiond (Mar 11 2021 at 12:26):Is abstract supposed to work in tactic-in-terms? The documentation says that it does not work "properly". But does that mean that it does not work at all? Obviously, it cannot work if there are evars lying around, but I cannot even make it work in the fully determined case. Here is a very simplified example:
Definition foo : { x | x = _ } :=
ltac:(exists 0; refine (_: _=0); abstract reflexivity).
Unfortunately, the proof of reflexivity is not abstracted away. Notice that I cannot use the proof mode here, because the type of the definition is not yet fully determined.
Enrico Tassi (Mar 11 2021 at 13:08):Internally, there is no reason for not letting one start a definition in interactive mode when the type is not fully ground. I'd recommend lifting this limitation (and make many other used happy I believe) rather than hacking with abstract and tacinterms
Enrico Tassi (Mar 11 2021 at 13:11):Maybe you could try Program Definition...
Guillaume Melquiond (Mar 11 2021 at 15:30):No, Program Definition does not help, because it requires that the term (even with holes) has a ground type, just like Definition. Or, perhaps I am misunderstanding what you mean.
Enrico Tassi (Mar 11 2021 at 15:58):You are right. One more reason to lift the limitation.
Matthieu Sozeau (Mar 19 2021 at 11:27):Indeed, this limitation is pretty bad.
Last updated: Oct 03 2023 at 19:01 UTC