-- The default include path should contain Agda.Primitive module TestDefaultIncludePath where import Agda.Primitive -- That's it.