All Questions
Tagged with agda pattern-matching
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
4
votes
2
answers
212
views
Binding variables to terms involving later variables
Consider the following pseudocode in a hypothetical proof assistant:
def f (n : ℕ) : P n
:= match n with
| zero -> ?0
| suc k -> ?1
end
...
- 3,200