search

omega12345 / RefactorAgda

Master's thesis project: A refactoring engine for Agda. Very much under construction.
BSD 3-Clause "New" or "Revised" License
6 stars 1 forks source link

Build failure: == not in scope #1

Open andreasabel opened 5 years ago

andreasabel commented 5 years ago

Trying to build RefactorAgda, I run into the following problem:

RefactorAgdaEngine/ParseTreeOperations.agda:48,114-116
Not in scope:
  ==
  at RefactorAgdaEngine/ParseTreeOperations.agda:48,114-116
when scope checking ==

OK, I think the problem is that I am using a different version of the standard-library. I need to add import

open import Data.String.Unsafe

See https://github.com/agda/agda-stdlib/issues/506