[Agda] Display of private things (for higher inductive types)

[Nils Anders Danielsson]

On 2012-08-13 10:47, Guillaume Brunerie wrote:
> By the way, I noticed that there is a part in the wiki about my exact
> problem, here:
>
> http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Modules#private
>
> It is said that it’s in general very hard to know how to display the
> normal form of a term involving private definitions.
> But I’m not sure I understand why, what about reducing the term as
> long a no private definition appear and decide that the normal form to
> be displayed is the last one not involving a private definition?

What about unification?

I recently wrote about something related:

   Re: evaluation in compilation
   http://thread.gmane.org/gmane.comp.lang.agda/4262/focus=4263

-- 
/NAD