liao zhang (Jun 16 2020 at 14:53): liao zhang (Jun 16 2020 at 14:53):I am confused with what role does KerName plays in tactic sentence.
“auto” is referred by KerName.
Does it mean all the KerName in tactic sentence point to some internal tactics like “auto”?
Is there any argument point by KerName? For example “apply X”, which X is pointed by KerName?
Pierre-Marie Pédrot (Jun 16 2020 at 16:33):only global tactics, like the one you define via Ltac foo := ... have a kernel name
liao zhang (Jun 16 2020 at 20:55):Pierre-Marie Pédrot said:
only global tactics, like the one you define via
Ltac foo := ...have a kernel name
Thanks very much!
Last updated: Oct 03 2023 at 04:02 UTC