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

5 votes
2 answers
204 views

What is a context mapping in dependent type checking?

2 votes
1 answer
185 views

What is a pattern in dependent pattern matching?

1 vote
1 answer
68 views

Use proof irrelevance in cast

1 vote
0 answers
58 views

Embedding proof assistance in an application

2 votes
1 answer
58 views

Eliminating dependent destruction in Coq

2 votes
1 answer
122 views

Provable `fun-ext`and "rewriting under binders" in intensional MLTT

1 vote
1 answer
86 views

Type of Sets with an Assocaitive Operation in Lean

32 votes
3 answers
1k views

What are the bases for different Proof Assistants?

2 votes
2 answers
134 views

What if identity type in extensional type theory were possibly non-deterministic?

3 votes
1 answer
80 views

Tricks for proving equalities under type cast

4 votes
1 answer
168 views

Co-induction principle

3 votes
2 answers
211 views

How to abstract over function arity in Lean and Coq?

17 votes
3 answers
585 views

Bringing OOP features into proof assistants?

4 votes
3 answers
261 views

Rewrite with definitional equality and dependent types

Browse more Questions