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

6 votes
1 answer
146 views

Termination and confluence -- which goes first?

6 votes
0 answers
126 views

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

6 votes
2 answers
402 views

How to run Agda?

20 votes
0 answers
333 views

Categorical semantics of Agda

1 vote
1 answer
88 views

Agda - Help with importing Haskell function via FFI

6 votes
1 answer
109 views

What are the differences and similarities between records, coinductive records, and codatatypes?

8 votes
1 answer
201 views

Why is `--irrelevant-projections` unsafe in Agda?

5 votes
0 answers
100 views

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

5 votes
1 answer
149 views

Why can termination checker affect strict Prop in Agda?

15 votes
2 answers
282 views

What are the upsides and downsides of typed vs untyped conversion?

1 vote
0 answers
154 views

Descriptions of heterogenous datatypes

5 votes
1 answer
135 views

How to convince Agda that definition is terminating in the presence of unapplied recursion?

7 votes
2 answers
223 views

Proving strict positivity in Agda

1 vote
1 answer
138 views

Does Agda's --injective-type-constructors flag have canonicity?

Browse more Questions