[Agda] Expose more of Agda to reflection?

[Ulf Norell]

On Wed, Feb 3, 2016 at 12:07 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> By "expose aggsy", I guess I mean that there would be a new function, agsy
> : Term → TC ⊤. Or maybe Term → TC Term. I'd rather not pursue this,
> however, as I think a much stronger case could be made for exposing
> "rewrite" than for agsy.
>
> I've taken a look at checkRHS, as Jesper suggested and I see now that
> there's a more fundamental problem than exposing "rewrite": there is no way
> to define a function without explicitly-stated patterns. E.g., in the Agda
> language, one can define:
>
>   foo : ∀ {X : Set} → {a b : X} → (a≡b : a ≡ b) → Set
>   foo refl = {!!}
>
> and Agda fills-in the implicit patterns as
>
>   foo {X} {a} {.a} refl = {!!}
>
> Using reflection's defineFun, one must specify all of the implicit
> patterns, as in the second form.
>

That'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't do is give implicit
arguments by name.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160203/c61b54cf/attachment.html