[Agda] Not Unfolding Local Defs

[Harley Eades III]

Hi, Jon.

> On May 11, 2016, at 10:31 AM, Jon Sterling <jon at jonmsterling.com> wrote:
> 
> There is also this experimental(?) DISPLAY pragma that can be used to
> force the expression to be displayed in the folded form. I have not
> tried it, but perhaps the following would work?
> 
> {-# DISPLAY _≤M_ m n = m ≤M n #-}

This is what I was hoping for.  I had not seen this before.  Thanks!

It seems the example you give doesn’t actually work, because it makes 
the display recursive, but what I could do was:

{-# DISPLAY rel = _≤M_ #-}

and it does what I want.  :-)

This is extremely helpful!

It also works for terms in types.

> Darin Morrison has been using DISPLAY very heavily in his recent Agda
> developments, and he says it has (along with other things) helped him
> make gnarly goals easier to read (see
> https://github.com/freebroccolo/agda-prelude for instance).

Thanks for the link.

Best,
Harley

> 
> Best,
> Jon
> 
> 
> On Tue, May 10, 2016, at 10:26 AM, Harley Eades III wrote:
>> Hi, everyone.
>> 
>> I am using a ton of records in my formalization, and at the top of
>> each module I give several convince definitions for the projections
>> of my records to make types easier to read.
>> 
>> For example, see the top of this file:
>> 
>> https://github.com/heades/dialectica-spaces/blob/Lambek/NCDialSets.agda
>> 
>> A typical example is the following:
>> 
>> _≤M_ : M → M → Set
>> _≤M_ = (rel (poset (oncMonoid bp-pf)))
>> 
>> This definition makes reading types a lot easier, but this definition is
>> unfolded
>> in goals, which makes the goal very hard to read.  Multiply this with a
>> number 
>> of definitions like this, and we get goals that are close to impossible
>> to read.
>> 
>> So I spend a lot of time trying to parse a goal myself to be able to do
>> the proof.
>> 
>> Is there a way to tell Agda not to unfold these definitions in goals?
>> 
>> Thanks,
>> Harley
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda