[Agda] Closures

[Nils Anders Danielsson]

On 2009-09-22 19:30, Vag Vagoff wrote:
>> 10 seconds for what?
> 
> In Emacs,
> 5 seconds if compiling/typechecking one module repeatedly,
> 9-10 seconds if compiling/typechecking one module after working on 
> another module.
> 
> In command line,
> compilation always takes 5 seconds, typechecking always takes 3 seconds.

Type-checking times vary widely from module to module; I would be very
happy if type-checking never took longer than 10 seconds. :)

> Here, in function `execute', arguments of local functions in double
> pars ((...)) is added to make compilation successful. Without them
> compiler complains by message " Type Σ != Σ' ". How to remove
> arguments in double parenthesis?

Stop quantifying over Σ and Ω in the local functions:

   execute {Σ} {Ω} input machine = …
    where

       loadTape : List Σ → Tape Σ
       ⋮

-- 
/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.