Skip to main content

Questions tagged [usage]

Questions asking how to properly and efficiently use Proof Assistants.

3 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
10 votes
0 answers
175 views

What are the practical differences between intensional and extensional type theories?

It is already proved that MLTT with equality reflection is equivalent to MLTT with an intensional equality, plus UIP and function extensionality. So theoretically the differences between intensional ...
Trebor's user avatar
  • 4,015
3 votes
0 answers
38 views

.CoqMakefile.d required by CoqMakefile but not generated

I am trying to use CoqMakefile to automatically build my Coq project in Coq 8.15.2. When I did this the compilation failed because a file ".CoqMakefile.d" was expected by make but did not ...
Rincewind's user avatar
  • 106
2 votes
1 answer
150 views

Debug autorewrite in Coq

I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting) I then manually figure out which rewrite rules were ...
8bc3 457f's user avatar
  • 224