Ticket #11 (new enhancement)

Opened 9 years ago

Hidden arguments in abstract syntax

Reported by: PeterLjunglof Owned by:
Priority: major Version:
Keywords: Cc:


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";
Note: See TracTickets for help on using tickets.