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
1 view

Agda: Cannot Instantiate Metavariable

6 votes
2 answers
78 views

Does ST$\lambda$C equal to simple type theory?

3 votes
1 answer
48 views

How does conversion check on partial elements/systems (in terms of cubical) work?

1 vote
1 answer
44 views

How does substitution on partial elements/systems (in terms of cubical) work?

2 votes
0 answers
26 views

Is there any work on the use of free logic in proof assistants?

13 votes
1 answer
181 views

How do Coq's bidirectionality hints (`&`) affect type checking?

7 votes
2 answers
173 views

How to access local definitions in Agda

3 votes
1 answer
51 views

Use of modal logic in metaprogramming

6 votes
1 answer
74 views

Tactic unification vs evarconv in Coq

0 votes
1 answer
70 views

Can a Prop show that all entries of a list equal Type@{U} for any U?

4 votes
1 answer
190 views

Formal description of Coq’s termination checker

3 votes
2 answers
155 views

Coq defining a hierarchy of collections of integers with infinitely many "levels"

14 votes
3 answers
745 views

Do you need a Hilbert style Epsilon operator for definitions in set theory?

5 votes
1 answer
150 views

Define a new Type in Lean: Tensor power of vector space

Browse more Questions