<div dir="ltr"><div><div><div><div>Hi Manny,<br><br></div>"Solve constraints" (C-c C-s) only works when Agda can see that there is a *unique* solution for a given hole. But the meaning of 'unique' here is a bit subtle: it considers `<>` to be different from, say, `if b then <> else <>`, even though the latter will evaluate to `<>` for any value of b. Technically speaking, Agda requires the solution to be unique up to definitional equality.<br><br></div>If you define One as a record type instead of as a datatype, then Agda will replace any value of type One (such as `if b then <> else <>`) by `<>`. This is called the eta rule for One. Agda has eta-rules built-in for record types but not for datatypes. So the following should work:<br><br>---------------<br>
<br>
record One : Set where<br>
  constructor <><br>
<br>
idOne : One -> One<br>
idOne <> = ?<br>
<br>
----------------<br><br></div>I assume the tutorials you read used the definition of One as a record type instead of as a datatype, which is why C-c C-s works in their case. I hope this helps!</div><div><br></div><div>cheers,</div><div>Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jan 5, 2018 at 7:44 PM, Manny Romero <span dir="ltr"><<a href="mailto:mannyromero@mail.com" target="_blank">mannyromero@mail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I'm very new on Emacs. (And everything else, for that matter!) While doing various Agda tutorials (not messing about with Emacs or anything) I'd noticed lately that sometimes the "solve constraints" command (C-c C-s in a hole) wouldn't work when the tutorial said it should. Sometimes I'd find the problem would go away in a future Emacs session, but it has returned and doesn't seem to be going away.<br>
<br>
To be sure about it, I started a new Emacs session and opened a new file where I wrote:<br>
<br>
---------------<br>
<br>
data One : Set where<br>
  <> : One<br>
<br>
idOne : One -> One<br>
idOne <> = ?<br>
<br>
----------------<br>
<br>
and loaded to create the hole at "?". Then I go in the hole, and C-c C-s doesn't work! Neither does C-c C-=. All other commands seem to work. I can use C-c C-f and C-c C-b to navigate into the hole; I can use C-c C-, and C-c C-. to give me information. I used C-c C-c in the first place on "idOne x = {!!}" to case split on x and get the present program. I can even, indeed, use C-c C-r on the present program to fill the hole automatically (as well as C-c C-SPC to fill it manually). And so forth. But I just can't get C-c C-s or C-c C-= to work (or the corresponding dropdown menu options), under this or any circumstance!<br>
<br>
What might be going on? How might I troubleshoot?<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>