Duplicate binding for built-in thing LEVEL

rodrigogribeiro / agda-software-foundations

Porting of software foundations book to Agda

37 stars 5 forks source link

Duplicate binding for built-in thing LEVEL #6

Open dredozubov opened 7 years ago

dredozubov commented 7 years ago

When I'm trying to load Basics.lagda, I get:

/Users/dr/workspace/agda-software-foundations/Basics.lagda:343,1-28

Duplicate binding for built-in thing LEVEL, previous binding to
.Agda.Primitive.Level
when checking the pragma BUILTIN LEVEL Level

rodrigogribeiro commented 7 years ago

I'll upload the fix for this today. This error is due to a change on how Agda deal with level stuff.