Timeline for Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 15 at 16:15 | comment | added | James Wood | In a sense, dot patterns can never introduce variables, but they sometimes are the most convenient or clearest place to introduce variables (after undotting). | |
| Mar 15 at 15:32 | comment | added | ice1000♦ |
@JamesWood I think the implicits are introduced in the pattern s<s {m} {n} m<n instead of the prior dotted patterns, but yeah you can also undot them
|
|
| Mar 15 at 9:54 | comment | added | James Wood |
I think the other half of the answer is that Agsy doesn't have any way to deal with the variables it wants to use not being in scope. The solution is to bring them into scope via either the s<s constructors' implicit arguments or by un-dotting the dot patterns and filling in the _s.
|
|
| Mar 15 at 3:17 | history | answered | ice1000♦ | CC BY-SA 4.0 |