[Agda] () is not a valid expression

[J.Burton at brighton.ac.uk]

At Wed, 19 Nov 2008 11:37:46 +0000,
Nils Anders Danielsson wrote:
> 
> On 2008-11-19 00:29, J.Burton at brighton.ac.uk wrote:
> > I was using emacs and AFAIK I must be using the latest version
> 
> Can you show us the output in your *ghci* buffer?
>
When I open load a module that just contains

open import Data.Bool

this what's in *ghci*:

GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude> :set -package Agda
package flags have changed, ressetting and loading new packages...
Loading package mtl-1.1.0.2 ... linking ... done.
Loading package old-locale-1.0.0.0 ... linking ... done.
Loading package old-time-1.0.0.0 ... linking ... done.
Loading package random-1.0.0.0 ... linking ... done.
Loading package QuickCheck-2.1.0.1 ... linking ... done.
Loading package array-0.1.0.0 ... linking ... done.
Loading package bytestring-0.9.1.3 ... linking ... done.
Loading package containers-0.1.0.1 ... linking ... done.
Loading package binary-0.4.4 ... linking ... done.
Loading package filepath-1.1.0.0 ... linking ... done.
Loading package directory-1.0.0.0 ... linking ... done.
Loading package unix-2.3.0.0 ... linking ... done.
Loading package process-1.0.0.0 ... linking ... done.
Loading package haskell98 ... linking ... done.
Loading package pretty-1.0.0.0 ... linking ... done.
Loading package haskell-src-1.0.1.3 ... linking ... done.
Loading package readline-1.0.1.0 ... linking ... done.
Loading package zlib-0.5.0.0 ... linking ... done.
Loading package Agda-2.1.3 ... linking ... done.
Prelude> :mod + Agda.Interaction.GhciTop
Prelude Agda.Interaction.GhciTop> cmd_reset
Prelude Agda.Interaction.GhciTop> cmd_load "/tmp/Test.agda" ["/home/jim/agda/lib", "/home/jim/sdf-git/dsel/agda", "."]
agda2_mode_code (agda2-status-action "")
agda2_mode_code (agda2-status-action "")
agda2_mode_code (agda2-status-action "")
Checking Data.Bool ( /home/jim/agda/lib/Data/Bool.agda )
Skipping Data.Function ( /home/jim/agda/lib/Data/Function.agdai )
Skipping Data.Sum ( /home/jim/agda/lib/Data/Sum.agdai )
Skipping Data.Empty ( /home/jim/agda/lib/Data/Empty.agdai )
Skipping Relation.Nullary.Core ( /home/jim/agda/lib/Relation/Nullary/Core.agdai )
Skipping Data.Product ( /home/jim/agda/lib/Data/Product.agdai )
Skipping Relation.Binary.Core ( /home/jim/agda/lib/Relation/Binary/Core.agdai )
Skipping Relation.Binary.Consequences.Core ( /home/jim/agda/lib/Relation/Binary/Consequences/Core.agdai )
Skipping Relation.Binary.PropositionalEquality.Core ( /home/jim/agda/lib/Relation/Binary/PropositionalEquality/Core.agdai )
Skipping Relation.Binary.Consequences ( /home/jim/agda/lib/Relation/Binary/Consequences.agdai )
Skipping Relation.Binary ( /home/jim/agda/lib/Relation/Binary.agdai )
Skipping Relation.Binary.PreorderReasoning ( /home/jim/agda/lib/Relation/Binary/PreorderReasoning.agdai )
Skipping Relation.Binary.EqReasoning ( /home/jim/agda/lib/Relation/Binary/EqReasoning.agdai )
Skipping Relation.Binary.FunctionLifting ( /home/jim/agda/lib/Relation/Binary/FunctionLifting.agdai )
Skipping Relation.Binary.PropositionalEquality ( /home/jim/agda/lib/Relation/Binary/PropositionalEquality.agdai )
Skipping Data.Unit ( /home/jim/agda/lib/Data/Unit.agdai )
agda2_mode_code (annotation-goto
                 '("/home/jim/agda/lib/Data/Bool.agda" . 1419))
agda2_mode_code (agda2-highlight-reload)
agda2_mode_code (agda2-status-action "")
agda2_mode_code (agda2-info-action
                 "*Error*"
                 "/home/jim/agda/lib/Data/Bool.agda:65,25-27
() is not a valid expression.
when scope checking ()")
*** Exception: exit: ExitFailure 1
Prelude Agda.Interaction.GhciTop> 
 

Jim

> -- 
> /NAD
> 
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses, which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081119/b2c2523d/attachment.html