Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our questions

0 votes
0 answers
3 views

Coq makefile complains about extension points on Windows 10

0 votes
3 answers
125 views

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

0 votes
1 answer
50 views

What is the difference between these inductive definitions in Coq?

1 vote
0 answers
68 views

Unfolding constants while rewriting using rewrite_strat and a hint database

4 votes
1 answer
106 views

What is the best way to learn Iris completely independently

0 votes
0 answers
16 views

reference ospecialize and variable prim_base_irreducible not found in the current environment

1 vote
1 answer
84 views

problem with unification

0 votes
0 answers
56 views

How to check a Zenon-generated proof with Coq?

1 vote
1 answer
63 views

How to express that two equivalence relations can setoid rewrite across each other (Coq)

0 votes
1 answer
131 views

Induction COQ Question

3 votes
2 answers
198 views

Universe inconsistency errors when using ZF model in Coq

0 votes
1 answer
134 views

Why inductive types (or variants) are so rigid in terms of the set of constructors

2 votes
2 answers
93 views

Continue a section (with context) in coq

2 votes
0 answers
27 views

Problem working with FMapWeakList and Parametrized Records

Browse more Questions