UlfNorell
commented
10 years ago From andreas....@gmail.com on October 14, 2013 07:45:03
Related to issue 528 and issue 532 and issue 434 .
Time for a clean implementation of the scope checker for record declarations.
Status: Accepted
Labels: Type-Defect Priority-Medium Record
From pumpkingod@gmail.com on October 08, 2013 03:56:26
The code below generates a parse error in the current state, but if you switch it to ! x y = x it parses fine.
module Bug where
record A : Set₁ where ! : Set → Set → Set x ! y = x -- Fails like this, but parses if ! is written prefix here
field bar : Set
{- Could not parse the left-hand side x ! y when scope checking let mutual ! : Set → Set → Set x ! y = x in (bar : Set) → Set₀ -}
Original issue: http://code.google.com/p/agda/issues/detail?id=917