[Agda] type annotation in-place

[Nils Anders Danielsson]

On 2015-10-08 16:57, Andrew Pitts wrote:
> OK, I get the general idea. But it would be nice to see an explanation
> of the semantics of this at a higher level than could be got by
> examining the relevant parts of the Haskell code -- I don't suppose
> there is one?

No, there is no formal semantics, other than the source code.

> Ditto for the "private" keyword (which I know from bitter experience
> only guarantees a certain amount of privacy, because of the way Agda
> pattern matching works
> <http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/#comment-80163>).

At least "private" is described on the wiki page that you linked to.

-- 
/NAD