Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
70
questions
6
votes
0
answers
232
views
Can Agda proofs be trusted and do they conform to a specific, well-defined type theory?
When using Agda proofs, how can you know whether to trust it? Also, do they conform to a specific, well-defined type theory?
Credit
- 1,338
8
votes
1
answer
159
views
Is it possible to define `fib` coinductive stream w/o sized types?
In Agda with --guardedness, we can define productive definitions using copatterns like the following
...
- 6,316
4
votes
1
answer
171
views
Why does Agda's `--without-K` option also affect the indices of inductive types, where they have to be of lower levels?
In my understanding, --without-K changes the index unification algorithm so that deletion rules are no longer used, as described in Jesper Cockx' "pattern ...
- 6,316
26
votes
4
answers
2k
views
What are the differences between MLTT and CIC?
In the theory and design of proof assistants based upon dependent types, I feel like there’s a somewhat cultural divide between the "MLTT" world (with Agda as the main representative proof ...
- 5,530
15
votes
2
answers
421
views
In Agda, why is universe polymorphism explicit?
I've noticed that the process of coding a definition in Agda that is universe polymorphic usually requires little thought in how the Level parameters are specified. ...
- 361
14
votes
1
answer
445
views
Why did Agda give up cumulative universes?
In Ulf Norell's PhD thesis, which is considered the standard reference of the Agda 2 language, the universes are cumulative, say, Set i is not just an instance of <...
- 6,316
7
votes
1
answer
176
views
How to state and prove the associativity of append of sized vectors with homogeneous equality?
Append (denoted ++) for sized vectors is obviously associative, i.e. a ++ (b ++ c) = (a ++ b) ++ c for ...
- 6,316
4
votes
1
answer
73
views
When installing Agda does one have to be attentive to a version?
If I want to install Agda do I have to be attentive to versions, breaking changes, etc.?
A comment from an earlier question noted
Agda version for installed libraries
- 2,846
6
votes
1
answer
169
views
Does Agda have breaking changes?
Since Agda is software and sometimes software has breaking changes, e.g. Python 2 vs Python 3 (ref), does Agda have any significant breaking changes that one would need to be concerned about?
Also ...
- 2,846
7
votes
3
answers
1k
views
How to run Agda?
I want to run Agda, but I do not know how to run functions. I need to run "Hello, World!"; how can I do this?
- 245