Open UlfNorell opened 10 years ago
From andreas....@gmail.com on November 18, 2013 17:20:38
Mon Nov 18 18:16:43 EET 2013 Andreas Abel andreas.abel@ifi.lmu.de
Adding Size< to standard library. Used for coinduction with copatterns, as in:
record R (i : Size where field force : {j : Size< i} -> R j
Attachment: sizelt.patch
Original issue: http://code.google.com/p/agda/issues/detail?id=969
From andreas....@gmail.com on November 18, 2013 17:20:38
Mon Nov 18 18:16:43 EET 2013 Andreas Abel andreas.abel@ifi.lmu.de
Adding Size< to standard library. Used for coinduction with copatterns, as in:
record R (i : Size where field force : {j : Size< i} -> R j
Attachment: sizelt.patch
Original issue: http://code.google.com/p/agda/issues/detail?id=969