[Agda] Trying to load modules from Norell OPLSS tutorial

[Andreas Abel]

Manny,

you need to upgrade to a newer version of Agda.  The latest release is 
2.5.3.

 > 7,12 :  Parse error
 > constructor<ERROR>

This is because Agda 2.4 does not know about the "instance" keyword.

Alternatively, you could try to get an old version of Ulf's Prelude, the 
one he used for the OPLSS.  I have no clue if this is possible, though.

Best,
Andreas

On 02.12.2017 21:24, Manny Romero wrote:
> 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.
> 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
> -----------------------
> 
> module Prelude.Unit where
> open import Agda.Builtin.Unit public
> record ⊤′ {a} : Set a where
>    instance constructor tt
> -- To keep changes from compat-2.4.0 to a minimum.
> Unit = ⊤
> pattern unit = tt
> -------------------------
> and the screen below reads something like
> -------------------------
> 7,12 :  Parse error
> constructor<ERROR>
> tt
> --------------------------
> When I comment out the text of this file and save, an error message for 
> another Prelude file pops up.
> What might I be doing wrong? Surely there isn't really something wrong 
> with all these files? Why might this be happening to me?
> 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!
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/