<html><head></head><body><div style="font-family: Verdana;font-size: 12.0px;"><div>I'm trying to follow the OPLSS 2014 Agda tutorial. As seen in the first two minutes here ( https://www.youtube.com/watch?v=NrSW7YsneVg ), this requires loading some files from agda-summer-school-OPLSS and agda-prelude on this ( https://github.com/UlfNorell/agda-summer-school ) website.</div>
<div> </div>
<div>Despite not knowing anything about computers, I think I've somehow managed to both download these files and tell emacs where to look for them successfully. The problem is that I now get error messages for Prelude files when I try to load Day1.agda. For instance, when I do so, the main screen shows "module Prelude.Unit where" followed by the rest of Unit.agda from the Prelude subdirectory</div>
<div> </div>
<div>
<div>-----------------------</div>
<div><br/>
module Prelude.Unit where</div>
<div>open import Agda.Builtin.Unit public</div>
<div>record ⊤′ {a} : Set a where<br/>
instance constructor tt</div>
<div>-- To keep changes from compat-2.4.0 to a minimum.<br/>
Unit = ⊤<br/>
pattern unit = tt</div>
</div>
<div> </div>
<div>-------------------------</div>
<div> </div>
<div>and the screen below reads something like</div>
<div> </div>
<div>-------------------------</div>
<div> </div>
<div>7,12 : Parse error</div>
<div>constructor<ERROR></div>
<div>tt</div>
<div> </div>
<div>--------------------------</div>
<div> </div>
<div>When I comment out the text of this file and save, an error message for another Prelude file pops up.</div>
<div> </div>
<div>What might I be doing wrong? Surely there isn't really something wrong with all these files? Why might this be happening to me?</div>
<div> </div>
<div>I have Linux Mint 18, Agda 2.4.2.5, Emacs 24.5.1. And again, I am completely computer illiterate and it's a minor miracle I managed to get this far!</div></div></body></html>