[Agda] Re: Syntax for anonymous functions

[Nils Anders Danielsson]

On 2011-05-24 21:52, Fredrik Nordvall Forsberg wrote:
> This is a bit heavyweight for a small function, though, so we have also
> introduced the syntax
>
>      (a , b) |->  a
>
> for one clause functions. The Unicode-inclined can use \mapsto in the
> emacs mode.

Adding both function and ↦ as keywords seems excessive to me. Would the
following syntax work?

   { p₁ ↦ e₁; p₂ ↦ e₂; … }

> By the way, am I the only one for which test/interaction/Issue373.agda
> doesn't output
>
>      [1 of 3] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
>      [2 of 3] Compiling Imports.Nat      ( Imports/Nat.hs, Imports/Nat.o )
>      [3 of 3] Compiling MAlonzo.Code.Issue373 ( MAlonzo/Code/Issue373.hs,
>                                                 MAlonzo/Code/Issue373.o )
>
> when running the test suite?

I get the following output (in Issue373.out):

   agda2_mode_code (agda2-status-action "")
   [1 of 3] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
   [2 of 3] Compiling Imports.Nat      ( Imports/Nat.hs, Imports/Nat.o )
   [3 of 3] Compiling MAlonzo.Code.Issue373 ( MAlonzo/Code/Issue373.hs, MAlonzo/Code/Issue373.o )
   agda2_mode_code (agda2-status-action "Checked")
   agda2_mode_code (agda2-info-action
                    "*Compilation result*"
                    "The module was successfully compiled.")
   agda2_mode_code (agda2-goals-action '())
   ok

> Or who gets the error message
>
>      Not implemented: primQNameType
>
> when compiling std-lib/src/Reflection.agdai in the compiler tests?

I think some people tend to skip the compiler test suite—it can take
roughly an hour to run, so that is not very strange. We should use a
quicker test (which also includes the Epic backend). Contributions are
welcome.

-- 
/NAD