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
1 answer
466 views

Examples of theories where tactic language is required for simple proofs

7 votes
0 answers
83 views

How to improve/understand typechecking performance in Agda?

6 votes
2 answers
208 views

Is there a formalism of "coinductive" data types with negative occurrences?

4 votes
2 answers
299 views

Reasoning about CwFs in a proof assistant

2 votes
2 answers
96 views

Inspecting proof terms in Agda

15 votes
1 answer
788 views

What are the complex induction patterns supported by Agda?

5 votes
0 answers
135 views

What are the conditions for Agda to detect that induction-recursion has a least fixed point?

3 votes
1 answer
114 views

Cumulativity unsafe in Agda 2.6.3

1 vote
1 answer
134 views

When we can use refl?

3 votes
2 answers
764 views

How to prove f x < f y → x ≢ y

0 votes
2 answers
86 views

Proof of state updating

2 votes
1 answer
68 views

How to write if_then_else function that accepts a type argument explicitly?

8 votes
1 answer
199 views

Termination and confluence -- which goes first?

7 votes
0 answers
173 views

What was the first proof assistant with eta equality for records?

Browse more Questions