I could not find par:
in the tactic index. Is it missing?
It's not a tactic, it's a selector https://coq.github.io/doc/master/refman/proof-engine/ltac.html#grammar-token-toplevel-selector
and what about [> ... | ... ]
? is it a tactic?
or +
?
but ok, anyway I was looking for its documentation, so thanks for the pointer
[> bla]
is ltac syntax https://coq.github.io/doc/master/refman/proof-engine/ltac.html#local-application-of-tactics
If by +
you mean bullets they're commands https://coq.github.io/doc/master/refman/proof-engine/proof-handling.html#bullets
and yet, they seem to be in the tactic index
Last updated: Oct 13 2024 at 01:02 UTC