Open UlfNorell opened 10 years ago
UlfNorell
commented
10 years ago From andreas....@gmail.com on November 22, 2013 01:46:53
This gives a proper error now. TODO: make Agsy work with copatterns.
Summary: Auto missing support for Copatterns (was: Internal error in Auto, due to missing support for Copatterns)
Labels: -Type-Defect Type-Enhancement
UlfNorell
commented
10 years ago From andreas....@gmail.com on November 29, 2013 07:38:32
I talked to Fredrik today and he thinks it is not worth spending time on the current Auto since he has a new one. He will do this after his thesis submission (sometime in Feb maybe)?
So, no milestone for 2.3.4.
Labels: -Milestone-2.3.4
UlfNorell
commented
10 years ago From andreas....@gmail.com on November 29, 2013 07:39:07
Owner: freli...@gmail.com
From andreas....@gmail.com on November 13, 2013 23:03:31
git clone git@github.com:andreasabel/cubical.git -b 0.0.0.1
Load cubical/src/Control/Auto-Bug-in-Goal-2.agda
Fix the module name (should be Control.Auto-Bug-in-Goal-2). Go to the second goal (?1). Press C-c C-a.
An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/Auto/Convert.hs:585
Original issue: http://code.google.com/p/agda/issues/detail?id=957