Skip to main content

Explore our questions

4 votes
3 answers
197 views

Which proof assistants implement Church's rule?

0 votes
1 answer
58 views

Proving a disjunction without left nor right in Coq

5 votes
1 answer
405 views

Why are dependent sums and products called sums and products?

2 votes
2 answers
84 views

Error when making CoqProject

3 votes
0 answers
25 views

Best tool for proving that a (big) first order model is actually the model of some (big) first order theory.

user avatar
1 vote
1 answer
33 views

Why the result of pattern matching don't get propagated in some expressions?

3 votes
1 answer
166 views

Can a metamath identifier be reused across scopes?

0 votes
2 answers
261 views

Induction COQ Question

0 votes
2 answers
41 views

Coq: how to apply "only once"

2 votes
1 answer
31 views

Induction over multiple arguments in Isabelle

3 votes
1 answer
147 views

Coq: unfold a class nested in the goal

2 votes
1 answer
91 views

Coq: when to give a context variable of imported package as argument

0 votes
1 answer
128 views

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

0 votes
1 answer
38 views

No notations from custom entries inside the proof state

Browse more Questions