Questions tagged [coq]

Coq is a formal proof management system. It is often referred to as a proof assistant.

Filter by
Sorted by
Tagged with
18 votes
1 answer

When to use coinductive types?

One could define streams in the following manner ...
user avatar
14 votes
1 answer

Converting between formulations of reals in Coq

While trying to answer more concretely a question on floating points, I tried proving a simple statement using the Flocq library of Coq. However, I got stuck before really exercising it because I am ...
user avatar
34 votes
2 answers

What are the main differences between Coq and Lean?

Coq and Lean are two of the most common proof assistants out there (but the question of course applies to other proof assistants too). What are the main differences between Coq and Lean? Ideally it ...
user avatar
  • 593
10 votes
1 answer

What are the differences between jsCoq and the versions of Coq that can be downloaded?

I found a site where I can use Coq in my browser: jsCoq Interactive Online System. Are there any major differences between the experience I'm getting on this site and the downloadable version(s)?
user avatar
  • 201