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