search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Need matching against record patterns for type-checking copatterns #959

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 14, 2013 00:39:48

git clone git@github.com:andreasabel/cubical.git -b 0.0.0.3

Load cubical/src/Control/Decoration.agda

look for --FAILS

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

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 21, 2013 22:34:43

There was no bug in record pattern translation, but we need to match against record patterns before the translation has been run. Fixed that.

Summary: Need matching against record patterns for type-checking copatterns (was: Bug in record pattern translation in connection with copatterns)
Status: Fixed
Labels: PatternMatching