<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 3, 2016 at 12:07 AM, Martin Stone Davis <span dir="ltr">&lt;<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>By &quot;expose aggsy&quot;, I guess I mean that there would be a new function, agsy : Term → TC ⊤. Or maybe Term → TC Term. I&#39;d rather not pursue this, however, as I think a much stronger case could be made for exposing &quot;rewrite&quot; than for agsy.<br><br></div>I&#39;ve taken a look at checkRHS, as Jesper suggested and I see now that there&#39;s a more fundamental problem than exposing &quot;rewrite&quot;: there is no way to define a function without explicitly-stated patterns. E.g., in the Agda language, one can define:<br><br>  foo : ∀ {X : Set} → {a b : X} → (a≡b : a ≡ b) → Set<br>  foo refl = {!!}<br><br></div>and Agda fills-in the implicit patterns as<br><br></div>  foo {X} {a} {.a} refl = {!!}<br><div><div><br></div><div>Using reflection&#39;s defineFun, one must specify all of the implicit patterns, as in the second form.</div></div></div></blockquote></div><br></div><div class="gmail_extra">That&#39;s not true. You can leave out the implicit patterns in defineFun. The clauses you give to defineFun are (of course) run through the type checker before being accepted, which includes all the machinery to figure out where implicit arguments go. The only thing you can&#39;t do is give implicit arguments by name.</div><div class="gmail_extra"><br></div><div class="gmail_extra">/ Ulf</div></div>