id,summary,reporter,owner,description,type,status,priority,version,resolution,keywords,cc
11,Hidden arguments in abstract syntax,PeterLjunglof,,"Hidden arguments a la Agda/Cayenne is nice.

E.g., lights are both switchable and dimmable:
{{{
fun light : (dev:DeviceType) -> Device(dev);
}}}
The first argument has to be in the lin definition, unused:
{{{
lin light _ = ...
}}}
Better would be to be able to say that `DeviceType` is a hidden argument, e.g.:
{{{
fun light : (dev:DeviceType) |-> Device dev;
lin light = ...
}}}
Another example, with both hidden and ordinary arguments:
{{{
fun request : (menu:Menu) |-> Action menu -> Utterance;
lin request act = ""i want to"" ++ act ++ ""please"";
}}}



",enhancement,new,major,,,,