3
$\begingroup$

One can read the Coq documentation about discriminate tactic here.

Were is this tactic actually defined?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ It's a builtin, it seems to be defined here at discr_tac. See also here. $\endgroup$
    – Couchy
    Commented Jul 7, 2022 at 6:41
  • $\begingroup$ Thank you! I'm interested in developing a bit more precise understanding of how tactics transform terms in the proof environment. I've seen some LTAC and I think it would be interesting to see how tactics operate under the hood. $\endgroup$
    – Jacob woolcutt
    Commented Jul 8, 2022 at 12:26

0

Reset to default

Browse other questions tagged or ask your own question.