# What is a hammer/atp within the logic of coq that does things like induction in coq?

**URL:** <https://discourse.rocq-prover.org/t/what-is-a-hammer-atp-within-the-logic-of-coq-that-does-things-like-induction-in-coq/1608>\
**Category:** Using Rocq\
**Created:** [March 24, 2022, 8:54pm UTC](https://discourse.rocq-prover.org/t/what-is-a-hammer-atp-within-the-logic-of-coq-that-does-things-like-induction-in-coq/1608 "2022-03-24T20:54:10Z")\
**Posts on this page:** 1\
**Showing post:** 2

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [March 24, 2022, 8:55pm UTC](https://discourse.rocq-prover.org/t/what-is-a-hammer-atp-within-the-logic-of-coq-that-does-things-like-induction-in-coq/1608/2 "2022-03-24T20:55:11Z")

</div>

just saw this: [Inductive proof automation](https://discourse.rocq-prover.org/t/inductive-proof-automation/226)

---

_[View the full topic](https://discourse.rocq-prover.org/t/what-is-a-hammer-atp-within-the-logic-of-coq-that-does-things-like-induction-in-coq/1608)._