[Agda] Not Unfolding Local Defs

[Yorick Sijsling]

As Wouter says,the abstract keyword may be useful. I used it here for
example:
https://github.com/yoricksijsling/PiWare-prefixes/blob/master/src/PiWarePrefixes/Patterns/Fan.lagda
.

The pattern i used is like this:

fan-impl : ∀ n → Circ n n
fan-impl n = ...

abstract
  fan : ∀ n → Circ n n
  fan n = fan-impl n

  reveal-fan : ∀ n → fan n ≡ fan-impl n
  reveal-fan n = refl

When the abstractly defined fan is used within a term it is treated similar
to a postulated definition. The actual definition is only unfolded within
the same abstract block. I can rewrite by reveal-fan to manually unfold the
definition of fan, which is necessary for a few proofs. By using this
pattern together with only a few proofs which used reveal-fan, i never had
to see anything of the implementation. It also solved some performance
issues in my case because the terms did not grow as large as before.

The DISPLAY pragma recognizes a pattern and displays it differently after
the fact, while abstract definitions never get expanded at all.

Yorick

On Thu, May 12, 2016 at 8:37 AM, Wouter Swierstra <w.s.swierstra at uu.nl>
wrote:

> > Is there a way to tell Agda not to unfold these definitions in goals?
>
> Have you tried using the abstract keyword? I seem to remember that it
> can be used prevent the definition being unfolded (but I can't seem to
> find any documentation).
>
>   Wouter
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160512/184e3e77/attachment.html