[Agda] Simple DepType Pattern Matching

[Wouter Swierstra]

Hi Yuya,

Try the following definition:

> f : Ty unit -> Unit
> f (ty .unit) = unit


You need to use a "dot pattern" in the pattern match. You can read  
more about this on the Agda wiki:

http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.DatatypeAndFunctionDefinitions

Hope this helps,

   Wouter