Where can I find the implementation for the SSreflect case tactic? Or some paper with the specifications for the SSreflect tactics?
What do you want to do exactly?
I'd like to make a diagram explaining how does case analysis work in Coq (like managing the goals) as simple as possible.
I'm not sure if SSReflect case depends on Coq's or destruct.
It does not
The main differences are:
case tactic shares most of its code with
elim. While the eliminator for
case is standard (given by Coq),
elim accepts a larger class of induction principles.
And there's some paper where its specification it's explained?
Something like this one, that explains implementation of vm_compute, https://coq.inria.fr/refman/zebibliography.html#compiledstrongreduction
to my knowledge, SSR papers are all listed here (see "Tooling about SSReflect ..."): https://math-comp.github.io/papers.html
Last updated: Jan 29 2023 at 19:02 UTC