# \#faq

**URL:** https://discourse.rocq-prover.org/tag/faq/2.md

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

---

## [Why is Coq consistent? What is the intended semantics?](https://discourse.rocq-prover.org/t/why-is-coq-consistent-what-is-the-intended-semantics/347)

<div class="topic-metadata">

**Author:** [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Replies:** 21\
**Last updated:** [September 27, 2019, 10:40am UTC](https://discourse.rocq-prover.org/t/why-is-coq-consistent-what-is-the-intended-semantics/347 "2019-09-27T10:40:18Z")

</div>

This seems to be missing from the faq. I have a fairly good idea of the answer, but was surprised not to find this documented (in one place). Am I overlooking something?

---

## [Suggested Answers](https://discourse.rocq-prover.org/t/suggested-answers/932)

<div class="topic-metadata">

**Author:** [@Onorio](https://discourse.rocq-prover.org/u/Onorio)\
**Replies:** 1\
**Last updated:** [July 7, 2020, 1:28pm UTC](https://discourse.rocq-prover.org/t/suggested-answers/932 "2020-07-07T13:28:57Z")

</div>

I suspect this is probably a FAQ but I can’t seem to find it anywhere. Apologies in advance for the dumb question but are the suggested answers to the exercises in Software Foundations: Volume 1 Logical Foundations post…

---

## [Does flambda slow down Coq?](https://discourse.rocq-prover.org/t/does-flambda-slow-down-coq/484)

<div class="topic-metadata">

**Author:** [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Replies:** 8\
**Last updated:** [October 28, 2019, 3:29pm UTC](https://discourse.rocq-prover.org/t/does-flambda-slow-down-coq/484 "2019-10-28T15:29:58Z")

</div>

If I want coq to be fast, should I use flambda today? In my very quick and unscientific try, the resulting Coq 8.10.0 seems ~20% slower! There could be a million reasons or mistakes on my part, or my coq code might be od…

---

## [Safe mode checking nothing was admitted?](https://discourse.rocq-prover.org/t/safe-mode-checking-nothing-was-admitted/206)

<div class="topic-metadata">

**Author:** [@gallais](https://discourse.rocq-prover.org/u/gallais)\
**Replies:** 4\
**Last updated:** [June 16, 2019, 11:58pm UTC](https://discourse.rocq-prover.org/t/safe-mode-checking-nothing-was-admitted/206 "2019-06-16T23:58:46Z")

</div>

Apparently coqchk happily accepts admitted proofs. And I can’t find any command line option to tell Coq to complain about such unsafe features. Any help is welcomed!

---

## [How to represent mathematical structures in Coq?](https://discourse.rocq-prover.org/t/how-to-represent-mathematical-structures-in-coq/188)

<div class="topic-metadata">

**Author:** [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Replies:** 7\
**Last updated:** [March 9, 2019, 12:01pm UTC](https://discourse.rocq-prover.org/t/how-to-represent-mathematical-structures-in-coq/188 "2019-03-09T12:01:16Z")

</div>

For the sake of example, let’s say I want to represent semigroups in Coq. There are quite a few different ways to go about this. A semigroup is a set plus a binary operation, which is associative. Record Sg := { C : …