Funny behaviour of @_

Status: Beta

Brought to you by: ccoquand, ikegamidaisuke, mbenke, n-kato, t-seino

#1 Funny behaviour of @_

Milestone: v1.0_(example)

Status: open

Owner: nobody

Labels: Typechecker (3)

Priority: 5

Updated: 2004-11-24

Created: 2004-11-24

Creator: Anonymous

Private: No

Omitting the @_ can save your day!
Look at the attached file...

> agdachecker bug.agda
bug.agda: Fail: (Position "bug.agda" 33 54,ErrMsg:Error
in the definition of fail1 because:
Constructor type is not a data: ?16)

> agdachecker bug.agda
bug.agda: Fail: (Position "bug.agda" 34 57,ErrMsg:Error
in the definition of fail2 because:
Constructor type is not a data: ?16)

The error message is quite obscure...

Andreas

Discussion

Nobody/Anonymous - 2004-11-24

Documentation of bug

bug.agda

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Funny behaviour of @_

Group

Searches

Help

#1 Funny behaviour of @_

Discussion