[Agda] Not Unfolding Local Defs

[Jon Sterling]

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 #-}

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).

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