Questions tagged [tactic]
A tactic is a command or instruction for constructing a formal proof by applying a common proof technique. For questions about high-level techniques for constructing proofs, use the tag (strategy).
2
questions
6
votes
2
answers
209
views
When is the lean 4 "by" required?
I am reading an introductory math/lean course here, and got confused about when the tactic/keyword by is required. It is used most of the time, but is occasionally ...
- 2,320
21
votes
2
answers
1k
views
What's the difference between reflection and tactics?
Agda has a reflection mechanism (not equality reflection or reflexivity, but something related to metaprogramming based on goals and contexts to generate terms) and people have developed some ...
- 6,346