Website
Documentation
Community
GitHub
Bug reports
Wiki
Coq
What is a hammer/atp within the logic of coq that does things like induction in coq?
Using Coq
brando90
March 24, 2022, 8:55pm
2
just saw this:
Inductive proof automation
show post in topic
Related Topics
Topic
Replies
Views
Activity
CoqHammer 1.1.1 for Coq 8.9
Announcements
14
1241
February 23, 2020
Thinking of using hammer/automation to guide the order of proving lemmas
Using Coq
0
368
October 24, 2021
Machine learning and hammers for Coq
Using Coq
45
6529
June 6, 2022
What does it mean that Isabelle has better automation than Coq?
Miscellaneous
15
3746
March 25, 2021
Inductive proof automation
Using Coq
6
966
March 25, 2022