Syntax \ {x = x} for named hidden abstraction missing

[UlfNorell]

From andreas....@gmail.com on April 18, 2011 13:41:33

It would be in line with the treatment of hidden application if there was also a syntax for selectively naming a hidden abstraction. For instance, in a place where something of type

forall {x y z} -> R x y -> R y z -> R x z

is expected, one might want to only refer to y and give a term like

\ {y = y'} Rxy Ryz -> bla(y')

Comments?

Original issue: http://code.google.com/p/agda/issues/detail?id=407

[UlfNorell]

From nils.anders.danielsson on April 22, 2011 03:52:40

I agree.

Status: Accepted
Cc: -nils.anders.danielsson
Labels: Type-Enhancement

[UlfNorell]

From ulf.nor...@gmail.com on September 03, 2011 00:57:07

Labels: Priority-Medium