MisspelledKeywordInRecord.agda 271 B

1234567891011121314
  1. -- Andreas, 2019-08-10
  2. record R : Set₁ where
  3. indutive
  4. field A : Set
  5. -- The error message is strange:
  6. -- This declaration is illegal in a record before the last field
  7. -- when scope checking the declaration
  8. -- record R where
  9. -- indutive
  10. -- field A : Set