Timeline for Where is the discriminate tactic defined in Coq?
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 8, 2022 at 12:26 | comment | added | Jacob woolcutt | 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. | |
| Jul 7, 2022 at 6:41 | comment | added | Couchy |
It's a builtin, it seems to be defined here at discr_tac. See also here.
|
|
| S Jul 7, 2022 at 2:26 | review | First questions | |||
| Jul 7, 2022 at 15:53 | |||||
| S Jul 7, 2022 at 2:26 | history | asked | Jacob woolcutt | CC BY-SA 4.0 |