Skip to main content

Explore our questions

3 votes
0 answers
66 views

Inductive from CoInductive?

0 votes
0 answers
107 views

Trouble proving a theorem using induction in Coq

1 vote
1 answer
54 views

How do I enable this kind of rewriting?

4 votes
1 answer
216 views

Dealing an equality with coq. - beginner's question

0 votes
1 answer
56 views

Coq, Merging two forall definitions ranging over the same types

2 votes
1 answer
80 views

How to use a lemma that is defined in a Coq module?

0 votes
1 answer
92 views

How to prove commutation of a recursive function over a finite set encoded with binary nat in coq

5 votes
2 answers
913 views

How do I express a negative premise in Coq?

5 votes
0 answers
150 views

Coq - Are there functions which are provably equal but not definitionally equal?

2 votes
1 answer
65 views

Packaging Mathematical Structures in Coq: Help Understanding a Definition

3 votes
2 answers
49 views

What is the most ergonomic way to eliminate multiple similar goals in Coq?

4 votes
2 answers
87 views

what symbols can I use in coq?

2 votes
4 answers
370 views

LEM, the halting problem, the curry-howard correspondence -> deep connection?

0 votes
0 answers
48 views

Analysis of proof that for a category which is also a poset, every diagram commutes

Browse more Questions