Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
70
questions
3
votes
0
answers
113
views
Lower bounds in type theory proof assistant with ordinals and universes without axioms
I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024?
My ...
- 279
2
votes
2
answers
144
views
Inspecting proof terms in Agda
In Coq, if I am unsure how a definition foo is defined, I can use the command Print foo. to inspect what ...
- 5,530
2
votes
1
answer
126
views
How to write if_then_else function that accepts a type argument explicitly?
While this function example works by declaring type A implicitly between brackets,
...
- 123
2
votes
1
answer
54
views
Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?
I am trying to prove the transitivity of <. But I got stuck as the proof found by Auto (...
- 2,220
1
vote
1
answer
376
views
Why does Agda use Set instead of Type?
In the 'Hello world' example in Agda — Agda 2.6.5 documentation, it straightforwardly uses Set as follows:
‘Hello world’ in Agda — Agda 2.6.5 documentation
...
- 161
1
vote
1
answer
135
views
Agda - Help with importing Haskell function via FFI
I'm trying out Agda's Foreign Function Interface with a simple correctness proof of quicksort (which I have defined in Haskell), but I'm having trouble importing the Haskell function. I've been ...
- 13
1
vote
1
answer
300
views
Does Agda's --injective-type-constructors flag have canonicity?
Since 2010/01/07, when the Anti-classicality of Agda was proved by Chung-Kil Hur, Agda's --injective-type-constructors is separated from the main branch of Agda (...
- 279
1
vote
1
answer
202
views
When we can use refl?
I am confused with the context related to identity type in HoTT
In particular, for a family $C : (a =_A a) \to U$ dependent on a loop, we cannot apply path induction and consider only the case for $C(...
- 181
1
vote
0
answers
180
views
Descriptions of heterogenous datatypes
When attempting to describe the datatype as appearing in my previous question, using indexed descriptions in style of The Gentle Art of Levitation to describe this datatype (using Agda for examples):
<...
- 547
0
votes
2
answers
88
views