[Agda] Not Unfolding Local Defs

[Harley Eades III]

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