[Agda] Data.Nat error

Ruben Henner Zilibowitz rzilibowitz at yahoo.com.au
Fri Nov 7 20:31:34 CET 2008


Hi,

I'm getting an error from importing the Data.Nat module from the  
standard library.

Checking Data.Nat ( /Users/rhz/Documents/dev/Agda/lib/Data/Nat.agda )
/Users/rhz/Documents/dev/Agda/lib/Data/Nat.agda:144,23-23
/Users/rhz/Documents/dev/Agda/lib/Data/Nat.agda:144,23: Parse error
)<ERROR> suc m ≟ zero = no \() ≤-pr...

Any help is appreciated...

Strangely I noticed that if I use the library in the AFP08 darcs  
repository instead, it appears to work without errors.

Regards,

Ruben



More information about the Agda mailing list