Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
70
questions
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
3
votes
1
answer
135
views
Cumulativity unsafe in Agda 2.6.3
I've been reading and understand the design choices behind Agda not having a cumulative universe hierarchy by default. However, while tinkering with the language, I've noticed that, at least for Agda ...
- 133
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
3
votes
2
answers
777
views
0
votes
2
answers
88
views
6
votes
2
answers
236
views
Is there a formalism of "coinductive" data types with negative occurrences?
Consider the following program in Haskell:
...
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
18
votes
1
answer
1k
views
What are the complex induction patterns supported by Agda?
A question was recently asked on the Coq-club mailing list on Coq rejecting a nastily nested inductive type. We encountered a similar difficulty while trying to port code from Agda to Coq: Agda ...
- 5,530
7
votes
0
answers
195
views
What was the first proof assistant with eta equality for records?
The Agda language supports eta equality for (non-(co)inductive) record types:
...
- 506
8
votes
1
answer
241
views
Termination and confluence -- which goes first?
I'm implementing a version of cubical type theory where the well-definedness of pattern matching functions is implied by:
the well-typedness of the clauses (type check)
the coverage of the patterns (...
- 6,316
23
votes
0
answers
571
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 3,200
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
9
votes
1
answer
362
views
What are the differences and similarities between records, coinductive records, and codatatypes?
Record types are a common feature in most paradigms.
Agda also allows defining records with the coinductive keyword.
Lastly there are the seemingly more exotic co(...
- 319
5
votes
0
answers
168
views
What are the conditions for Agda to detect that induction-recursion has a least fixed point?
This is a 3rd in a series of questions, spurred by my attempts to encode an argument by Danielsson [1] [2] regarding existence of syntactically non-strictly positive datatype.
The idea (rephrased):
...
- 547
6
votes
1
answer
200
views
Why can termination checker affect strict Prop in Agda?
In https://dl.acm.org/doi/10.1145/3290316 section 4 (which I believe is a standard reference), the authors claimed that Voevodsky's propositional resizing rule justifies the consistency of an ...
- 6,316