search

gallais / idris-tparsec

TParsec - Total Parser Combinators in Idris
https://gallais.github.io/idris-tparsec/
GNU General Public License v3.0
93 stars 10 forks source link

Compile error in recordChar: No such variable ignore #15

Closed epost closed 5 years ago

epost commented 5 years ago

Hi, I stumbled upon the following problem when compiling (@clayrat):

erik@munin:~/dev/3rdparty/idris-tparsec (master) $ idris --build TParsec.ipkg
Entering directory `./src'
Type checking ./Relation/Indexed.idr
Type checking ./Relation/Subset.idr
Type checking ./Induction/Nat.idr
Type checking ./Data/SizedDict.idr
Type checking ./Data/Inspect.idr
Type checking ./Data/DList.idr
Type checking ./Data/NEList.idr
Type checking ./TParsec/Result.idr
Type checking ./TParsec/Success.idr
Type checking ./TParsec/Types.idr
./TParsec/Types.idr:109:16-56:
    |
109 | recordChar c = MkTPT $ ignore (modify (mapFst (next c)))
    |                ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of recordChar with expected type
        TParsecT e a m ()

When checking argument runTPT to constructor TParsec.Types.MkTPT:
        No such variable ignore
gallais commented 5 years ago

Hi Erik,

ignore was moved to Prelude in February so I'm guessing you are using an older version of Idris. A possible solution would be to upgrade to Idris 1.3.0 which was released in May and thus includes the change.

epost commented 5 years ago

Hi, you're right, it was a version thing. Thanks for replying, problem solved!