agda/doc/release-notes/2.5.2.md

Release notes for Agda version 2.5.2

Installation and infrastructure

• Modular support for literate programming

Literate programming support has been moved out of the lexer and into the Agda.Syntax.Parser.Literate module.

Files ending in .lagda are still interpreted as literate TeX. The extension .lagda.tex may now also be used for literate TeX files.

Support for more literate code formats and extensions can be added modularly.

By default, .lagda.* files are opened in the Emacs mode corresponding to their last extension. One may switch to and from Agda mode manually.

• reStructuredText

Literate Agda code can now be written in reStructuredText format, using the .lagda.rst extension.

As a general rule, Agda will parse code following a line ending in ::, as long as that line does not start with ... The module name must match the path of the file in the documentation, and must be given explicitly. Several files have been converted already, for instance:

• language/mixfix-operators.lagda.rst
• tools/compilers.lagda.rst

Note that:

• Code blocks inside an rST comment block will be type-checked by Agda, but not rendered in the documentation.
• Code blocks delimited by .. code-block:: agda will be rendered in the final documenation, but not type-checked by Agda.
• All lines inside a codeblock must be further indented than the first line of the code block.

• Indentation must be consistent between code blocks. In other words, the file as a whole must be a valid Agda file if all the literate text is replaced by white space.

• Documentation testing

All documentation files in the doc/user-manual directory that end in .lagda.rst can be typechecked by running make user-manual-test, and also as part of the general test suite.

• Support installation through Stack

The Agda sources now also include a configuration for the stack install tool (tested through continuous integration).

It should hence be possible to repeatably build any future Agda version (including unreleased commits) from source by checking out that version and running stack install from the checkout directory. By using repeatable builds, this should keep selecting the same dependencies in the face of new releases on Hackage.

For further motivation, see Issue #2005.

• Removed the --test command-line option

This option ran the internal test-suite. This test-suite was implemented using Cabal supports for test-suites. [Issue #2083].

• The --no-default-libraries flag has been split into two flags [Issue #1937]

  • --no-default-libraries: Ignore the defaults file but still look for local .agda-lib files
  • --no-libraries: Don't use any .agda-lib files (the previous behaviour of --no-default-libraries).

• If agda was built inside git repository, then the --version flag will display the hash of the commit used, and whether the tree was -dirty (i.e. there were uncommited changes in the working directory). Otherwise, only the version number is shown.

Language

• Dot patterns are now optional

Consider the following program

  data Vec (A : Set) : Nat → Set where
    []   : Vec A zero
    cons : ∀ n → A → Vec A n → Vec A (suc n)

  vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
  vmap .zero    f []            = []
  vmap .(suc m) f (cons m x xs) = cons m (f x) (vmap m f xs)

If we don't care about the dot patterns they can (and could previously) be replaced by wildcards:

  vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
  vmap _ f []            = []
  vmap _ f (cons m x xs) = cons m (f x) (vmap m f xs)

Now it is also allowed to give a variable pattern in place of the dot pattern. In this case the variable will be bound to the value of the dot pattern. For our example:

  vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
  vmap n f []            = []
  vmap n f (cons m x xs) = cons m (f x) (vmap m f xs)

In the first clause n reduces to zero and in the second clause n reduces to suc m.

• Module parameters can now be refined by pattern matching

Previously, pattern matches that would refine a variable outside the current left-hand side was disallowed. For instance, the following would give an error, since matching on the vector would instantiate n.

  module _ {A : Set} {n : Nat} where
    f : Vec A n → Vec A n
    f []       = []
    f (x ∷ xs) = x ∷ xs

Now this is no longer disallowed. Instead n is bound to the appropriate value in each clause.

• With-abstraction now abstracts also in module parameters

The change that allows pattern matching to refine module parameters also allows with-abstraction to abstract in them. For instance,

  module _ (n : Nat) (xs : Vec Nat (n + n)) where
    f : Nat
    f with n + n
    f    | nn = ? -- xs : Vec Nat nn

Note: Any function argument or lambda-bound variable bound outside a given function counts as a module parameter.

To prevent abstraction in a parameter you can hide it inside a definition. In the above example,

  module _ (n : Nat) (xs : Vec Nat (n + n)) where

    ys : Vec Nat (n + n)
    ys = xs

    f : Nat
    f with n + n
    f    | nn = ? -- xs : Vec Nat nn, ys : Vec Nat (n + n)

• As-patterns [Issue #78].

As-patterns (@-patterns) are finally working and can be used to name a pattern. The name has the same scope as normal pattern variables (i.e. the right-hand side, where clause, and dot patterns). The name reduces to the value of the named pattern. For example::

  module _ {A : Set} (_<_ : A → A → Bool) where
    merge : List A → List A → List A
    merge xs [] = xs
    merge [] ys = ys
    merge xs@(x ∷ xs₁) ys@(y ∷ ys₁) =
      if x < y then x ∷ merge xs₁ ys
               else y ∷ merge xs ys₁

• Idiom brackets.

There is new syntactic sugar for idiom brackets:

`(| e a1 .. an |)` expands to

`pure e <*> a1 <*> .. <*> an`

The desugaring takes place before scope checking and only requires names pure and _<*>_ in scope. Idiom brackets work well with operators, for instance

`(| if a then b else c |)` desugars to

`pure if_then_else_ <*> a <*> b <*> c`

Limitations:

- The top-level application inside idiom brackets cannot include
  implicit applications, so `(| foo {x = e} a b |)` is illegal. In
  the case `e` is pure you can write `(| (foo {x = e}) a b |)`
  which desugars to

    `pure (foo {x = e}) <*> a <*> b`

- Binding syntax and operator sections cannot appear immediately inside
  idiom brackets.

• Layout for pattern matching lambdas.

You can now write pattern matching lambdas using the syntax

  λ where false → true
          true  → false

avoiding the need for explicit curly braces and semicolons.

• Overloaded projections [Issue #1944].

Ambiguous projections are no longer a scope error. Instead they get resolved based on the type of the record value they are eliminating. This corresponds to constructors, which can be overloaded and get disambiguated based on the type they are introducing. Example:

  module _ (A : Set) (a : A) where

  record R B : Set where
    field f : B
  open R public

  record S B : Set where
    field f : B
  open S public

Exporting f twice from both R and S is now allowed. Then,

  r : R A
  f r = a

  s : S A
  f s = f r

disambiguates to:

  r : R A
  R.f r = a

  s : S A
  S.f s = R.f r

If the type of the projection is known, it can also be disambiguated unapplied.

  unapplied : R A -> A
  unapplied = f

• Postfix projections [Issue #1963].

Agda now supports a postfix syntax for projection application. This style is more in harmony with copatterns. For example:

  record Stream (A : Set) : Set where
    coinductive
    field head : A
          tail : Stream A

  open Stream

  repeat : ∀{A} (a : A) → Stream A
  repeat a .head = a
  repeat a .tail = repeat a

  zipWith : ∀{A B C} (f : A → B → C) (s : Stream A) (t : Stream B) → Stream C
  zipWith f s t .head = f (s .head) (t .head)
  zipWith f s t .tail = zipWith f (s .tail) (t .tail)

  module Fib (Nat : Set) (zero one : Nat) (plus : Nat → Nat → Nat) where

    {-# TERMINATING #-}
    fib : Stream Nat
    fib .head = zero
    fib .tail .head = one
    fib .tail .tail = zipWith plus fib (fib .tail)

The thing we eliminate with projection now is visibly the head, i.e., the left-most expression of the sequence (e.g. repeat in repeat a .tail).

The syntax overlaps with dot patterns, but for type correct left hand sides there is no confusion: Dot patterns eliminate function types, while (postfix) projection patterns eliminate record types.

By default, Agda prints system-generated projections (such as by eta-expansion or case splitting) prefix. This can be changed with the new option:

  {-# OPTIONS --postfix-projections #-}

Result splitting in extended lambdas (aka pattern lambdas) always produces postfix projections, as prefix projection pattern do not work here: a prefix projection needs to go left of the head, but the head is omitted in extended lambdas.

  dup : ∀{A : Set}(a : A) → A × A
  dup = λ{ a → ? }

Result splitting (C-c C-c RET) here will yield:

  dup = λ{ a .proj₁ → ? ; a .proj₂ → ? }

• Projection parameters [Issue #1954].

When copying a module, projection parameters will now stay hidden arguments, even if the module parameters are visible. This matches the situation we had for constructors since long. Example:

  module P (A : Set) where
    record R : Set where
      field f : A

  open module Q A = P A

Parameter A is now hidden in R.f:

  test : ∀{A} → R A → A
  test r = R.f r

Note that a module parameter that corresponds to the record value argument of a projection will not be hidden.

  module M (A : Set) (r : R A) where
    open R A r public

  test' : ∀{A} → R A → A
  test' r = M.f r

• Eager insertion of implicit arguments [Issue #2001]

Implicit arguments are now (again) eagerly inserted in left-hand sides. The previous behaviour of inserting implicits for where blocks, but not right-hand sides was not type safe.

• Module applications can now be eta expanded/contracted without changing their behaviour [Issue #1985]

Previously definitions exported using open public got the incorrect type for underapplied module applications.

Example:

  module A where
    postulate A : Set

  module B (X : Set) where
    open A public

  module C₁ = B
  module C₂ (X : Set) = B X

Here both C₁.A and C₂.A have type (X : Set) → Set.

• Polarity pragmas.

Polarity pragmas can be attached to postulates. The polarities express how the postulate's arguments are used. The following polarities are available:

_: Unused.

++: Strictly positive.

+: Positive.

-: Negative.

*: Unknown/mixed.

Polarity pragmas have the form

  {-# POLARITY name <zero or more polarities> #-}

and can be given wherever fixity declarations can be given. The listed polarities apply to the given postulate's arguments (explicit/implicit/instance), from left to right. Polarities currently cannot be given for module parameters. If the postulate takes n arguments (excluding module parameters), then the number of polarities given must be between 0 and n (inclusive).

Polarity pragmas make it possible to use postulated type formers in recursive types in the following way:

  postulate
    ∥_∥ : Set → Set

  {-# POLARITY ∥_∥ ++ #-}

  data D : Set where
    c : ∥ D ∥ → D

Note that one can use postulates that may seem benign, together with polarity pragmas, to prove that the empty type is inhabited:

  postulate
    _⇒_    : Set → Set → Set
    lambda : {A B : Set} → (A → B) → A ⇒ B
    apply  : {A B : Set} → A ⇒ B → A → B

  {-# POLARITY _⇒_ ++ #-}

  data ⊥ : Set where

  data D : Set where
    c : D ⇒ ⊥ → D

  not-inhabited : D → ⊥
  not-inhabited (c f) = apply f (c f)

  inhabited : D
  inhabited = c (lambda not-inhabited)

  bad : ⊥
  bad = not-inhabited inhabited

Polarity pragmas are not allowed in safe mode.

• Declarations in a where-block are now private. [Issue #2101] This means that

  f ps = body where
    decls

is now equivalent to

  f ps = body where
    private
      decls

This changes little, since the decls were anyway not in scope outside body. However, it makes a difference for abstract definitions, because private type signatures can see through abstract definitions. Consider:

  record Wrap (A : Set) : Set where
    field unwrap : A

  postulate
    P : ∀{A : Set} → A → Set

  abstract

    unnamedWhere : (A : Set) → Set
    unnamedWhere A = A
      where  -- the following definitions are private!
      B : Set
      B = Wrap A

      postulate
        b : B
        test : P (Wrap.unwrap b)  -- succeeds

The abstract is inherited in where-blocks from the parent (here: function unnamedWhere). Thus, the definition of B is opaque and the type equation B = Wrap A cannot be used to check type signatures, not even of abstract definitions. Thus, checking the type P (Wrap.unwrap b) would fail. However, if test is private, abstract definitions are translucent in its type, and checking succeeds. With the implemented change, all where-definitions are private, in this case B, b, and test, and the example succeeds.

Nothing changes for the named forms of where,

  module M where
  module _ where

For instance, this still fails:

  abstract

    unnamedWhere : (A : Set) → Set
    unnamedWhere A = A
      module M where
      B : Set
      B = Wrap A

      postulate
        b : B
        test : P (Wrap.unwrap b)  -- fails

• Private anonymous modules now work as expected [Issue #2199]

Previously the private was ignored for anonymous modules causing its definitions to be visible outside the module containing the anonymous module. This is no longer the case. For instance,

  module M where
    private
      module _ (A : Set) where
        Id : Set
        Id = A

    foo : Set → Set
    foo = Id

  open M

  bar : Set → Set
  bar = Id -- Id is no longer in scope here

• Pattern synonyms are now expanded on left hand sides of DISPLAY pragmas [Issue #2132]. Example:

  data D : Set where
    C c : D
    g : D → D

  pattern C′ = C

  {-# DISPLAY C′ = C′ #-}
  {-# DISPLAY g C′ = c #-}

This now behaves as:

  {-# DISPLAY C = C′ #-}
  {-# DISPLAY g C = c #-}

Expected error for

  test : C ≡ g C
  test = refl

is thus:

  C′ != c of type D

• The built-in floats have new semantics to fix inconsistencies and to improve cross-platform portability.

  • Float equality has been split into two primitives. primFloatEquality is designed to establish decidable propositional equality while primFloatNumericalEquality is intended for numerical computations. They behave as follows:

  primFloatEquality NaN NaN = True
  primFloatEquality 0.0 -0.0 = False
  
  primFloatNumericalEquality NaN NaN = False
  primFloatNumericalEquality 0.0 -0.0 = True
  

  This change fixes an inconsistency, see [Issue #2169]. For further detail see the user manual.

  • Floats now have only one NaN value. This is necessary for proper Float support in the JavaScript backend, as JavaScript (and some other platforms) only support one NaN value.

  • The primitive function primFloatLess was renamed primFloatNumericalLess.

• Added new primitives to built-in floats:

  • primFloatNegate : Float → Float [Issue #2194]

  • Trigonometric primitives [Issue #2200]:

  primCos   : Float → Float
  primTan   : Float → Float
  primASin  : Float → Float
  primACos  : Float → Float
  primATan  : Float → Float
  primATan2 : Float → Float → Float
  

• Anonymous declarations [Issue #1465].

A module can contain an arbitrary number of declarations named _ which will scoped-checked and type-checked but won't be made available in the scope (nor exported). They cannot introduce arguments on the LHS (but one can use lambda-abstractions on the RHS) and they cannot be defined by recursion.

  _ : Set → Set
  _ = λ x → x

Rewriting

• The REWRITE pragma can now handle several names. E.g.: agda {-# REWRITE eq1 eq2 #-}

Reflection

• You can now use macros in reflected terms [Issue #2130].

For instance, given a macro

  macro
    some-tactic : Term → TC ⊤
    some-tactic = ...

the term def (quote some-tactic) [] represents a call to the macro. This makes it a lot easier to compose tactics.

• The reflection machinery now uses normalisation less often:

  • Macros no longer normalise the (automatically quoted) term arguments.

  • The TC primitives inferType, checkType and quoteTC no longer normalise their arguments.

  • The following deprecated constructions may also have been changed: quoteGoal, quoteTerm, quoteContext and tactic.

• New TC primitive: withNormalisation.

To recover the old normalising behaviour of inferType, checkType, quoteTC and getContext, you can wrap them inside a call to withNormalisation true:

    withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A

• New TC primitive: reduce.

  reduce : Term → TC Term

Reduces its argument to weak head normal form.

• Added new TC primitive: isMacro [Issue #2182]

  isMacro : Name → TC Bool

Returns true if the name refers to a macro, otherwise false.

• The record-type constructor now has an extra argument containing information about the record type's fields: agda data Definition : Set where … record-type : (c : Name) (fs : List (Arg Name)) → Definition …

Type checking

• Files with open metas can be imported now [Issue #964]. This should make simultaneous interactive development on several modules more pleasant.

Requires option: --allow-unsolved-metas

Internally, before serialization, open metas are turned into postulates named

    unsolved#meta.<nnn>

where <nnn> is the internal meta variable number.

• The performance of the compile-time evaluator has been greatly improved.

  • Fixed a memory leak in evaluator (Issue #2147).

  • Reduction speed improved by an order of magnitude and is now comparable to the performance of GHCi. Still call-by-name though.

• The detection of types that satisfy K added in Agda 2.5.1 has been rolled back (see Issue #2003).

• Eta-equality for record types is now only on after the positivity checker has confirmed it is safe to have it. Eta-equality for unguarded inductive records previously lead to looping of the type checker. [See Issue #2197]

  record R : Set where
    inductive
    field r : R

    loops : R
    loops = ?

As a consequence of this change, the following example does not type-check any more:

  mutual
    record ⊤ : Set where

    test : ∀ {x y : ⊤} → x ≡ y
    test = refl

It fails because the positivity checker is only run after the mutual block, thus, eta-equality for ⊤ is not available when checking test.

One can declare eta-equality explicitly, though, to make this example work.

  mutual
    record ⊤ : Set where
      eta-equality

    test : ∀ {x y : ⊤} → x ≡ y
    test = refl

• Records with instance fields are now eta expanded before instance search.

For instance, assuming Eq and Ord with boolean functions _==_ and _<_ respectively,

    record EqAndOrd (A : Set) : Set where
      field {{eq}}  : Eq A
            {{ord}} : Ord A


    leq : {A : Set} {{_ : EqAndOrd A}} → A → A → Bool
    leq x y = x == y || x < y

Here the EqAndOrd record is automatically unpacked before instance search, revealing the component Eq and Ord instances.

This can be used to simulate superclass dependencies.

• Overlappable record instance fields.

Instance fields in records can be marked as overlappable using the new overlap keyword:

    record Ord (A : Set) : Set where
      field
        _<_ : A → A → Bool
        overlap {{eqA}} : Eq A

When instance search finds multiple candidates for a given instance goal and they are all overlappable it will pick the left-most candidate instead of refusing to solve the instance goal.

This can be use to solve the problem arising from shared "superclass" dependencies. For instance, if you have, in addition to Ord above, a Num record that also has an Eq field and want to write a function requiring both Ord and Num, any Eq constraint will be solved by the Eq instance from whichever argument that comes first.

    record Num (A : Set) : Set where
      field
        fromNat : Nat → A
        overlap {{eqA}} : Eq A

    lessOrEqualFive : {A : Set} {{NumA : Num A}} {{OrdA : Ord A}} → A → Bool
    lessOrEqualFive x = x == fromNat 5 || x < fromNat 5

In this example the call to _==_ will use the eqA field from NumA rather than the one from OrdA. Note that these may well be different.

• Instance fields can be left out of copattern matches [Issue #2288]

Missing cases for instance fields (marked {{ }}) in copattern matches will be solved using instance search. This makes defining instances with superclass fields much nicer. For instance, we can define Nat instances of Eq, Ord and Num from above as follows:

    instance
      EqNat : Eq Nat
      _==_ {{EqNat}} n m = eqNat n m

      OrdNat : Ord Nat
      _<_ {{OrdNat}} n m = lessNat n m

      NumNat : Num Nat
      fromNat {{NumNat}} n = n

The eqA fields of Ord and Num are filled in using instance search (with EqNat in this case).

• Limited instance search depth [Issue #2269]

To prevent instance search from looping on bad instances (see Issue #1743) the search depth of instance search is now limited. The maximum depth can be set with the --instance-search-depth flag and the default value is 500.

Emacs mode

• New command C-u C-u C-c C-n: Use show to display the result of normalisation.

Calling C-u C-u C-c C-n on an expression e (in a hole or at top level) normalises show e and prints the resulting string, or an error message if the expression does not normalise to a literal string.

This is useful when working with complex data structures for which you have defined a nice Show instance.

Note that the name show is hardwired into the command.

• Changed feature: Interactively split result.

Make-case (C-c C-c) with no variables will now either introduce function arguments or do a copattern split (or fail).

This is as before:

  test : {A B : Set} (a : A) (b : B) → A × B
  test a b = ?

  -- expected:
  -- proj₁ (test a b) = {!!}
  -- proj₂ (test a b) = {!!}

  testFun : {A B : Set} (a : A) (b : B) → A × B
  testFun = ?

  -- expected:
  -- testFun a b = {!!}

This is has changed:

  record FunRec A : Set where
    field funField : A → A
  open FunRec

  testFunRec : ∀{A} → FunRec A
  testFunRec = ?

  -- expected (since 2016-05-03):
  -- funField testFunRec = {!!}

  -- used to be:
  -- funField testFunRec x = {!!}

• Changed feature: Split on hidden variables.

Make-case (C-c C-c) will no longer split on the given hidden variables, but only make them visible. (Splitting can then be performed in a second go.)

  test : ∀{N M : Nat} → Nat → Nat → Nat
  test N M = {!.N N .M!}

Invoking splitting will result in:

  test {N} {M} zero M₁ = ?
  test {N} {M} (suc N₁) M₁ = ?

The hidden .N and .M have been brought into scope, the visible N has been split upon.

• Non-fatal errors/warnings.

Non-fatal errors and warnings are now displayed in the info buffer and do not interrupt the typechecking of the file.

Currently termination errors, unsolved metavariables, unsolved constraints, positivity errors, deprecated BUILTINs, and empty REWRITING pragmas are non-fatal errors.

• Highlighting for positivity check failures

Negative occurences of a datatype in its definition are now highlighted in a way similar to termination errors.

• The abbrev for codata was replaced by an abbrev for code environments.

If you type c C-x ' (on a suitably standard setup), then Emacs will insert the following text:

  \begin{code}<newline>  <cursor><newline>\end{code}<newline>.

• The LaTeX backend can now be invoked from the Emacs mode.

Using the compilation command (C-c C-x C-c).

The flag --latex-dir can be used to set the output directory (by default: latex). Note that if this directory is a relative path, then it is interpreted relative to the "project root". (When the LaTeX backend is invoked from the command line the path is interpreted relative to the current working directory.) Example: If the module A.B.C is located in the file /foo/A/B/C.agda, then the project root is /foo/, and the default output directory is /foo/latex/.

• The compilation command (C-c C-x C-c) now by default asks for a backend.

To avoid this question, set the customisation variable agda2-backend to an appropriate value.

• The command agda2-measure-load-time no longer "touches" the file, and the optional argument DONT-TOUCH has been removed.

• New command C-u (C-u) C-c C-s: Simplify or normalise the solution C-c C-s produces

When writing examples, it is nice to have the hole filled in with a normalised version of the solution. Calling C-c C-s on

  _ : reverse (0 ∷ 1 ∷ []) ≡ ?
  _ = refl

used to yield the non informative reverse (0 ∷ 1 ∷ []) when we would have hopped to get 1 ∷ 0 ∷ [] instead. We can now control finely the degree to which the solution is simplified.

• Changed feature: Solving the hole at point

Calling C-c C-s inside a specific goal does not solve all the goals already instantiated internally anymore: it only solves the one at hand (if possible).

• New bindings: All the blackboard bold letters are now available [Pull Request #2305]

The Agda input method only bound a handful of the blackboard bold letters but programmers were actually using more than these. They are now all available: lowercase and uppercase. Some previous bindings had to be modified for consistency. The naming scheme is as follows:

• \bx for lowercase blackboard bold
• \bX for uppercase blackboard bold
• \bGx for lowercase greek blackboard bold (similar to \Gx for greeks)

• \bGX for uppercase greek blackboard bold (similar to \GX for uppercase greeks)

• Replaced binding for go back

Use M-, (instead of M-*) for go back in Emacs ≥ 25.1 (and continue using M-* with previous versions of Emacs).

Compiler backends

• JS compiler backend

The JavaScript backend has been (partially) rewritten. The JavaScript backend now supports most Agda features, notably copatterns can now be compiled to JavaScript. Furthermore, the existing optimizations from the other backends now apply to the JavaScript backend as well.

• GHC, JS and UHC compiler backends

Added new primitives to built-in floats [Issues #2194 and #2200]:

  primFloatNegate : Float → Float
  primCos         : Float → Float
  primTan         : Float → Float
  primASin        : Float → Float
  primACos        : Float → Float
  primATan        : Float → Float
  primATan2       : Float → Float → Float

LaTeX backend

• Code blocks are now (by default) surrounded by vertical space. [Issue #2198]

Use \AgdaNoSpaceAroundCode{} to avoid this vertical space, and \AgdaSpaceAroundCode{} to reenable it.

Note that, if \AgdaNoSpaceAroundCode{} is used, then empty lines before or after a code block will not necessarily lead to empty lines in the generated document. However, empty lines inside the code block do (by default) lead to empty lines in the output.

If you prefer the previous behaviour, then you can use the agda.sty file that came with the previous version of Agda.

• \AgdaHide{...} now eats trailing spaces (using \ignorespaces).

• New environments: AgdaAlign, AgdaSuppressSpace and AgdaMultiCode.

Sometimes one might want to break up a code block into multiple pieces, but keep code in different blocks aligned with respect to each other. Then one can use the AgdaAlign environment. Example usage:

    \begin{AgdaAlign}
    \begin{code}
      code
        code  (more code)
    \end{code}
    Explanation...
    \begin{code}
      aligned with "code"
        code  (aligned with (more code))
    \end{code}
    \end{AgdaAlign}

Note that AgdaAlign environments should not be nested.

Sometimes one might also want to hide code in the middle of a code block. This can be accomplished in the following way:

    \begin{AgdaAlign}
    \begin{code}
      visible
    \end{code}
    \AgdaHide{
    \begin{code}
      hidden
    \end{code}}
    \begin{code}
      visible
    \end{code}
    \end{AgdaAlign}

However, the result may be ugly: extra space is perhaps inserted around the code blocks.

The AgdaSuppressSpace environment ensures that extra space is only inserted before the first code block, and after the last one (but not if \AgdaNoSpaceAroundCode{} is used).

The environment takes one argument, the number of wrapped code blocks (excluding hidden ones). Example usage:

    \begin{AgdaAlign}
    \begin{code}
      code
        more code
    \end{code}
    Explanation...
    \begin{AgdaSuppressSpace}{2}
    \begin{code}
      aligned with "code"
        aligned with "more code"
    \end{code}
    \AgdaHide{
    \begin{code}
      hidden code
    \end{code}}
    \begin{code}
        also aligned with "more code"
    \end{code}
    \end{AgdaSuppressSpace}
    \end{AgdaAlign}

Note that AgdaSuppressSpace environments should not be nested.

There is also a combined environment, AgdaMultiCode, that combines the effects of AgdaAlign and AgdaSuppressSpace.

Tools

agda-ghc-names

The agda-ghc-names now has its own repository at

https://github.com/agda/agda-ghc-names

and is no longer distributed with Agda.