All Questions
Tagged with agda implicit-argument
2
questions
2
votes
1
answer
53
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
3
votes
1
answer
138
views
Can I specify `refl`'s parameter explicitly in Agda?
I'm working on some proofs in Agda that, for educational purposes, explicitly use the path induction principle (which I've defined myself) rather than pattern matching. In the theoretical mathematical ...
- 319