All Questions
Tagged with automated-theorem-proving coq
1
question
4
votes
2
answers
186
views
Ltac - run tactic for each hypothesis of given pattern
Especially in the context of lia, which can sometimes fail to prove a theorem in the form of
forall x, x <> 0 -> P x
...
- 171