# Terms vs Theorem vs Formula in Coq?

**URL:** <https://discourse.rocq-prover.org/t/terms-vs-theorem-vs-formula-in-coq/503>\
**Category:** Using Rocq\
**Created:** [November 21, 2019, 5:44pm UTC](https://discourse.rocq-prover.org/t/terms-vs-theorem-vs-formula-in-coq/503 "2019-11-21T17:44:18Z")\
**Posts on this page:** 1\
**Showing post:** 3

<div class="post-metadata">

**Author:** ![Pinocchio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/pinocchio/32/398_2.png) [@Pinocchio](https://discourse.rocq-prover.org/u/Pinocchio)\
**Post date:** [December 18, 2019, 3:57pm UTC](https://discourse.rocq-prover.org/t/terms-vs-theorem-vs-formula-in-coq/503/3 "2019-12-18T15:57:07Z")

</div>

But in other theorem provers like, HOL Light, the distinction between a theorem and a term is rigorous. As I understand it, a term can only be of type theorem if it has actually been the output of a set of inference rules or tactics, but what I thought was weird is that Coq does not actually make this distinction explicit for some reason. Do you know why?

* * *

Wrote a related question: [Why doesn't Coq have a theorem Type like HOL Light?](https://discourse.rocq-prover.org/t/why-doesnt-coq-have-a-theorem-type-like-hol-light/532)

---

_[View the full topic](https://discourse.rocq-prover.org/t/terms-vs-theorem-vs-formula-in-coq/503)._