[Agda] Not Unfolding Local Defs

[Harley Eades III]

Hi, Yorick and Wouter.

Very sorry about the late reply.  Been swamped with finishing up the end of the semester.

The abstract keyword is quite nice, and since I essentially want to make notations
these do not ever need to be unfolded.  

So this might be a better fit for me.  

Thanks a lot for explaining this!

Best,
Harley

> On May 12, 2016, at 6:18 AM, Yorick Sijsling <yoricksijsling at gmail.com> wrote:
> 
> 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 <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 <mailto: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 <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
> 

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