Compilation error in Agda.TypeChecking.Reduce.appDefE'

UlfNorell / agda-test

Agda test

0 stars 0 forks source link

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From andres.s...@gmail.com on October 27, 2013 18:46:10

After the patch

Sun Oct 27 08:26:56 COT 2013 andreas.abel@ifi.lmu.de

Optimization for underapplied redex is wrong for copatterns and functions of flexible arity. Removed.

there is a compilation error:

$ make compile-emacs-mode ... src/full/Agda/TypeChecking/Reduce.hs:528:30: Not in scope: `n'

UlfNorell commented 10 years ago

From andres.s...@gmail.com on October 27, 2013 10:47:46

Labels: Type-Defect

UlfNorell commented 10 years ago

From andreas....@gmail.com on October 27, 2013 12:43:01

Ah, I overlooked the last build failure. Sorry. Fixing this.

UlfNorell commented 10 years ago

From andreas....@gmail.com on October 27, 2013 13:01:24

Fixed now.

Status: Fixed
Cc: -andreas....@gmail.com