Skip to main content

Explore our questions

1 vote
2 answers
214 views

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

26 votes
4 answers
1k views

What are the differences between MLTT and CIC?

6 votes
1 answer
99 views

What are the typechecking differences between records and iterated sigma types in Agda?

3 votes
2 answers
214 views

Has extensionality ever caused any problems in a mathematical proof?

3 votes
2 answers
248 views

How to convert Agda's with statement to a helper function?

2 votes
1 answer
50 views

Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?

3 votes
1 answer
381 views

How to provide proof for termination in Agda?

4 votes
2 answers
200 views

Binding variables to terms involving later variables

6 votes
1 answer
342 views

What are the principal differences between Agda's core type theory and Coq's?

2 votes
2 answers
139 views

Can Hyperreal exist a axiom-free implementation in HoTT?

7 votes
3 answers
957 views

How to run Agda?

6 votes
1 answer
546 views

Examples of theories where tactic language is required for simple proofs

7 votes
0 answers
95 views

How to improve/understand typechecking performance in Agda?

6 votes
2 answers
225 views

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

Browse more Questions