— Release notes for Agda 2 version 2.4.0

  Important changes since 2.3.2:

  Installation and Infrastructure

  * A new module called Agda.Primitive has been introduced. This module
    is available to all users, even if the standard library is not used.
    Currently the module contains level primitives and their
    representation in Haskell when compiling with MAlonzo:

      infixl 6 _⊔_

        Level : Set
        lzero : Level
        lsuc  : (ℓ : Level) → Level
        _⊔_   : (ℓ₁ ℓ₂ : Level) → Level

      {-# COMPILED_TYPE Level ()      #-}
      {-# COMPILED lzero ()           #-}
      {-# COMPILED lsuc  (\_ → ())   #-}
      {-# COMPILED _⊔_   (\_ _ → ()) #-}

      {-# BUILTIN LEVEL     Level  #-}
      {-# BUILTIN LEVELZERO lzero  #-}
      {-# BUILTIN LEVELSUC  lsuc   #-}
      {-# BUILTIN LEVELMAX  _⊔_    #-}

    To bring these declarations into scope you can use a declaration
    like the following one:

      open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

    The standard library reexports these primitives (using the names
    zero and suc instead of lzero and lsuc) from the Level module.

    Existing developments using universe polymorphism might now trigger
    the following error message:

      Duplicate binding for built-in thing LEVEL, previous binding to

    To fix this problem, please remove the duplicate bindings.

    Technical details (perhaps relevant to those who build Agda

    The include path now always contains a directory <DATADIR>/lib/prim,
    and this directory is supposed to contain a subdirectory Agda
    containing a file Primitive.agda.

    The standard location of <DATADIR> is system- and
    installation-specific.  E.g., in a cabal —user installation of
    Agda-2.3.4 on a standard single-ghc Linux system it would be
    $HOME/.cabal/share/Agda-2.3.4 or something similar.

    The location of the <DATADIR> directory can be configured at
    compile-time using Cabal flags (--datadir and —datasubdir).
    The location can also be set at run-time, using the Agda_datadir
    environment variable.

  Pragmas and Options

  * Pragma NO_TERMINATION_CHECK placed within a mutual block is now
    applied to the whole mutual block (rather than being discarded
    silently).  Adding to the uses 1.−4. outlined in the release notes
    for 2.3.2 we allow:

    3a. Skipping an old-style mutual block: Somewhere within ‘mutual’
        block before a type signature or first function clause.

           {-# NO_TERMINATION_CHECK #-}
           c : A
           c = d

           d : A
           d = c

  * New option —no-pattern-matching

    Disables all forms of pattern matching (for the current file).
    You can still import files that use pattern matching.

  * New option -v profile:7

    Prints some stats on which phases Agda spends how much time.
    (Number might not be very reliable, due to garbage collection
    interruptions, and maybe due to laziness of Haskell.)

  * New option —no-sized-types

    Option —sized-types is now default.
    —no-sized-types will turn off an extra (inexpensive) analysis on
    data types used for subtyping of sized types.


  TODO: Document quoteContext.

  * Experimental feature: Varying arity.
    Function clauses may now have different arity, e.g.,

      Sum : ℕ → Set
      Sum 0       = ℕ
      Sum (suc n) = ℕ → Sum n

      sum : (n : ℕ) → ℕ → Sum n
      sum 0       acc   = acc
      sum (suc n) acc m = sum n (m + acc)


      T : Bool → Set
      T true  = Bool
      T false = Bool → Bool

      f : (b : Bool) → T b
      f false true  = false
      f false false = true
      f true = true

    This feature is experimental.  Yet unsupported:
    * Varying arity and ‘with’.
    * Compilation of functions with varying arity to Haskell, JS, or Epic.

  * Experimental feature: copatterns.  (Activated with option —copatterns)

    We can now define a record by explaining what happens if you project
    the record.  For instance:

      {-# OPTIONS —copatterns #-}

      record __ (A B : Set) : Set where
        constructor _,_
          fst : A
          snd : B
      open __

      pair : {A B : Set} → A → B → A  B
      fst (pair a b) = a
      snd (pair a b) = b

      swap : {A B : Set} → A  B → B  A
      fst (swap p) = snd p
      snd (swap p) = fst p

      swap3 : {A B C : Set} → A  (B  C) → C  (B  A)
      fst (swap3 t)       = snd (snd t)
      fst (snd (swap3 t)) = fst (snd t)
      snd (snd (swap3 t)) = fst t

    Taking a projection on the left hand side (lhs) is called a
    projection pattern, applying to a pattern is called an application
    pattern.  (Alternative terms: projection/application copattern.)

    In the first example, the symbol ‘pair’, if applied to variable
    patterns a and b and then projected via fst, reduces to a.
    ‘pair’ by itself does not reduce.

    A typical application are coinductive records such as streams:

      record Stream (A : Set) : Set where
          head : A
          tail : Stream A
      open Stream

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

    Again, ‘repeat a’ by itself will not reduce, but you can take
    a projection (head or tail) and then it will reduce to the
    respective rhs.  This way, we get the lazy reduction behavior
    necessary to avoid looping corecursive programs.

    Application patterns do not need to be trivial (i.e., variable
    patterns), if we mix with projection patterns.  E.g., we can have

      nats : Nat → Stream Nat
      head (nats zero) = zero
      tail (nats zero) = nats zero
      head (nats (suc x)) = x
      tail (nats (suc x)) = nats x

    Here is an example (not involving coinduction) which demostrates
    records with fields of function type:

      — The State monad

      record State (S A : Set) : Set where
        constructor state
          runState : S → A  S
      open State

      — The Monad type class

      record Monad (M : Set → Set) : Set1 where
        constructor monad
          return : {A : Set}   → A → M A
          _>>=_  : {A B : Set} → M A → (A → M B) → M B

      — State is an instance of Monad
      — Demonstrates the interleaving of projection and application patterns

      stateMonad : {S : Set} → Monad (State S)
      runState (Monad.return stateMonad a  ) s  = a , s
      runState (Monad._>>=_  stateMonad m k) s₀ =
        let a , s₁ = runState m s₀
        in  runState (k a) s₁

      module MonadLawsForState {S : Set} where

        open Monad (stateMonad {S})

        leftId : {A B : Set}(a : A)(k : A → State S B) →
          (return a >>= k) ≡ k a
        leftId a k = refl

        rightId : {A B : Set}(m : State S A) →
          (m >>= return) ≡ m
        rightId m = refl

        assoc : {A B C : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
          ((m >>= k) >>= l) ≡ (m >>= λ a → (k a >>= l))
        assoc m k l = refl

    Copatterns are yet experimental and the following does not work:

    * Copatterns and ‘with’ clauses.

    * Compilation of copatterns to Haskell, JS, or Epic.

    * Projections generated by
        open R {{…}}
      are not handled properly on lhss yet.

    * Conversion checking is slower in the presence of copatterns,
      since stuck definitions of record type do no longer count
      as neutral, since they can become unstuck by applying a projection.
      Thus, comparing two neutrals currently requires comparing all
      they projections, which repeats a lot of work.

  * Top-level module no longer required.

    The top-level module can be omitted from an Agda file. The module name is
    then inferred from the file name by dropping the path and the .agda
    extension. So, a module defined in /A/B/C.agda would get the name C.

    You can also suppress only the module name of the top-level module by writing

      module _ where

    This works also for parameterised modules.

  * Module parameters are now always hidden arguments in projections.
    For instance:

      module M (A : Set) where

        record Prod (B : Set) : Set where
          constructor _,_
            fst : A
            snd : B
        open Prod public

      open M

    Now, the types of fst and snd are

      fst : {A : Set}{B : Set} → Prod A B → A
      snd : {A : Set}{B : Set} → Prod A B → B

    Until 2.3.2, they were

      fst : (A : Set){B : Set} → Prod A B → A
      snd : (A : Set){B : Set} → Prod A B → B

    This change is a step towards symmetry of constructors and projections.
    (Constructors always took the module parameters as hidden arguments).

  * Telescoping lets: Local bindings are now accepted in telescopes
    of modules, function types, and lambda-abstractions.

    The syntax of telescopes as been extended to support ‘let’:

      id : (let ★ = Set) (A : ★) → A → A
      id A x = x

    In particular one can now ‘open’ modules inside telescopes:

     module Star where
       ★ : Set₁
       ★ = Set

     module MEndo (let open Star) (A : ★) where
       Endo : ★
       Endo = A → A

    Finally a shortcut is provided for opening modules:

      module N (open Star) (A : ★) (open MEndo A) (f : Endo) where

    The semantics of the latter is

      module _ where
        open Star
        module _ (A : ★) where
          open MEndo A
          module N (f : Endo) where

    The semantics of telescoping lets in function types and lambda
    abstractions is just expanding them into ordinary lets.

  * More liberal left-hand sides in lets [Issue 1028]:

      You can now write left-hand sides with arguments also for let bindings
      without a type signature. For instance,

        let f x = suc x in f zero

      Let bound functions still can’t do pattern matching though.

  * Ambiguous names in patterns are now optimistically resolved in favor
    of constructors. [Issue 822] In particular, the following succeeds now:

      module M where

        data D : Set₁ where
          [_] : Set → D

      postulate [_] : Set → Set

      open M

      Foo : _ → Set
      Foo [ A ] = A

  * Anonymous where-modules are opened public. [Issue 848]

      f args = rhs
        module _ telescope where
      <more clauses>

    means the following (not proper Agda code, since you cannot put a
    module in-between clauses)

      module _ {arg-telescope} telescope where

      f args = rhs
      <more clauses>


      A : Set1
      A = B module _ where
        B : Set1
        B = Set

      C : Set1
      C = B

  * Builtin ZERO and SUC have been merged with NATURAL.

    When binding the NATURAL builtin, ZERO and SUC are bound to the appropriate
    constructors automatically. This means that instead of writing

      {-# BUILTIN NATURAL Nat #-}
      {-# BUILTIN ZERO zero #-}
      {-# BUILTIN SUC suc #-}

    you just write

      {-# BUILTIN NATURAL Nat #-}

  * Pattern synonym can now have implicit arguments. [Issue 860]

    For example,

      pattern tail=_ {x} xs = x ∷ xs

      len : ∀ Ā → List A → Nat
      len []         = 0
      len (tail= xs) = 1 + len xs

  * Syntax declarations can now have implicit arguments. [Issue 400]

    For example

      id : ∀ ā{A : Set a} → A → A
      id x = x

      syntax id Ā x = x ∈ A

  * Minor syntax changes

    * -} is now parsed as end-comment even if no comment was begun.
      As a consequence, the following definition gives a parse error

        f : {A- : Set} → Set
        f {A-} = A-

      because Agda now sees ID(f) LBRACE ID(A) END-COMMENT, and no
      longer ID(f) LBRACE ID(A-) RBRACE.

      The rational is that the previous lexing was to context-sensitive,
      attempting to comment-out f using {- and -} lead to a parse error.

    * Fixities (binding strengths) can now be negative numbers as
      well. [Issue 1109]

        infix −1 _myop_

    * Postulates are now allowed in mutual blocks. [Issue 977]

    * Empty where blocks are now allowed. [Issue 947]

    * Pattern synonyms are now allowed in parameterised modules. [Issue 941]

    * Empty hiding and renaming lists in module directives are now allowed.

    * Module directives using, hiding, renaming and public can now appear in
      arbitrary order. Multiple using/hiding/renaming directives are allowed, but
      you still cannot have both using and hiding (because that doesn’t make
      sense). [Issue 493]

  Goal and error display

  * The error message “Refuse to construct infinite term” has been
    removed, instead one gets unsolved meta variables.  Reason: the
    error was thrown over-eagerly. [Issue 795]

  * If an interactive case split fails with message

      Since goal is solved, further case distinction is not supported;
      try Solve constraints’ instead

    then the associated interaction meta is assigned to a solution.
    Press C-c C-= (Show constraints) to view the solution and C-c C-s
    (Solve constraints) to apply it. [Issue 289]

  Type checking

  * [ issue 376 ] Implemented expansion of bound record variables during meta assignment.
    Now Agda can solve for metas X that are applied to projected variables, e.g.:

      X (fst z) (snd z) = z

      X (fst z)         = fst z

    Technically, this is realized by substituting (x , y) for z with fresh
    bound variables x and y.  Here the full code for the examples:

      record Sigma (A : Set)(B : A → Set) : Set where
        constructor _,_
          fst : A
          snd : B fst
      open Sigma

      test : (A : Set) (B : A → Set) →
        let X : (x : A) (y : B x) → Sigma A B
            X = _
        in  (z : Sigma A B) → X (fst z) (snd z) ≡ z
      test A B z = refl

      test’ : (A : Set) (B : A → Set) →
        let X : A → A
            X = _
        in  (z : Sigma A B) → X (fst z) ≡ fst z
      test’ A B z = refl

    The fresh bound variables are named fst(z) and snd(z) and can appear
    in error messages, e.g.:

      fail : (A : Set) (B : A → Set) →
        let X : A → Sigma A B
            X = _
        in  (z : Sigma A B) → X (fst z) ≡ z
      fail A B z = refl

    results in error:

      Cannot instantiate the metavariable _7 to solution fst(z) , snd(z)
      since it contains the variable snd(z) which is not in scope of the
      metavariable or irrelevant in the metavariable but relevant in the
      when checking that the expression refl has type _7 A B (fst z) ≡ z

  * Dependent record types and definitions by copatterns require
    reduction with previous function clauses while checking the
    current clause. [Issue 907]

    For a simple example, consider

      test : ∀ Ā → Σ Nat λ n → Vec A n
      proj₁ test = zero
      proj₂ test = []

    For the second clause, the lhs and rhs are typed as

      proj₂ test : Vec A (proj₁ test)
      []         : Vec A zero

    In order for these types to match, we have to reduce the lhs type
    with the first function clause.

    Note that termination checking comes after type checking, so be
    careful to avoid non-termination!  Otherwise, the type checker
    might get into an infinite loop.

  * The implementation of the primitive primTrustMe has changed.
    It now only reduces to REFL if the two arguments x and y have
    the same computational normal form.  Before, it reduced when
    x and y were definitionally equal, which included type-directed
    equality laws such as eta-equality.  Yet because reduction is
    untyped, calling conversion from reduction lead to Agda crashes
    [Issue 882].

    The amended description of primTrustMe is (cf. release notes for 2.2.6):

      primTrustMe : {A : Set} {x y : A} → x ≡ y

    Here _≡_ is the builtin equality (see BUILTIN hooks for equality,

    If x and y have the same computational normal form, then
    primTrustMe{x=x}{y=y} reduces to refl.

    A note on primTrustMe’s runtime behavior:
    The MAlonzo compiler replaces all uses of primTrustMe with the
    REFL builtin, without any check for definitional equality. Incorrect
    uses of primTrustMe can potentially lead to segfaults or similar
    problems of the compiled code.

  * Implicit patterns of record type are now only eta-expanded if there
    is a record constructor. [Issues 473, 635]

      data D : Set where
        d : D

      data P : D → Set where
        p : P d

      record Rc : Set where
        constructor c
        field f : D

      works : {r : Rc} → P (Rc.f r) → Set
      works p = D

    This works since the implicit pattern {r} is eta-expanded to
    {c x} which allows the type of p to reduce to P x and x to be
    unified with d.  The corresponding explicit version is:

      works’ : (r : Rc) → P (Rc.f r) → Set
      works’ (c .d) p = D

    However, if the record constructor is removed, the same example will

      record R : Set where
        field f : D

      fails : {r : R} → P (R.f r) → Set
      fails p = D

      — d != R.f r of type D
      — when checking that the pattern p has type P (R.f r)

    The error is justified since there is no pattern we could write down
    for r.  It would have to look like

      record { f = .d }

    but anonymous record patterns are not part of the language.

  * Absurd lambdas at different source locations are no longer
    different. [Issue 857]
    In particular, the following code type-checks now:

      absurd-equality : _≡_ {A = ⊥ → ⊥} (λ()) λ()
      absurd-equality = refl

    Which is a good thing!

  * Printing of named implicit function types.

    When printing terms in a context with bound variables Agda renames new
    bindings to avoid clashes with the previously bound names. For instance, if A
    is in scope, the type (A : Set) → A is printed as (A₁ : Set) → A₁. However,
    for implicit function types the name of the binding matters, since it can be
    used when giving implicit arguments.

    For this situation, the following new syntax has been introduced:
    {x = y : A} → B is an implicit function type whose bound variable (in scope
    in B) is y, but where the name of the argument is x for the purposes of
    giving it explicitly. For instance, with A in scope, the type {A : Set} → A
    is now printed as {A = A₁ : Set} → A₁.

    This syntax is only used when printing and is currently not being parsed.

  * Changed the semantics of —without-K. [Issue 712, Issue 865, Issue 1025]

    New specification of —without-K:

    When —without-K is enabled, the unification of indices for pattern matching
    is restricted in two ways:

    1. Reflexive equations of the form x == x are no longer solved, instead Agda
       gives an error when such an equation is encountered.

    2. When unifying two same-headed constructor forms ‘c us’ and ‘c vs’ of type
       ‘D pars ixs’, the datatype indices ixs (but not the parameters) have to
       be *self-unifiable*, i.e. unification of ixs with itself should succeed
       positively. This is a nontrivial requirement because of point 1.


    * The J rule is accepted.

        J : {A : Set} (P : {x y : A} → x ≡ y → Set) →
            (∀ x → P (refl x)) →
            ∀ {x y} (x≡y : x ≡ y) → P x≡y
        J P p (refl x) = p x

      This definition is accepted since unification of x with y doesn’t require
      deletion or injectivity.

    * The K rule is rejected.

        K : {A : Set} (P : {x : A} → x ≡ x → Set) →
            (∀ x → P (refl {x = x})) →
           ∀ {x} (x≡x : x ≡ x) → P x≡x
        K P p refl = p _

      Definition is rejected with the following error:

        Cannot eliminate reflexive equation x = x of type A because K has
        been disabled.
        when checking that the pattern refl has type x ≡ x

    * Symmetry of the new criterion.

        test₁ : {k l m : ℕ} → k + l ≡ m → ℕ
        test₁ refl = zero

        test₂ : {k l m : ℕ} → k ≡ l + m → ℕ
        test₂ refl = zero

      Both versions are now accepted (previously only the first one was).

    * Handling of parameters.

        cons-injective : {A : Set} (x y : A) → (x ∷ []) ≡ (y ∷ []) → x ≡ y
        cons-injective x .x refl = refl

      Parameters are not unified, so they are ignored by the new criterion.

    * A larger example: antisymmetry of ≤.

        data _≤_ : ℕ → ℕ → Set where
          lz : (n : ℕ) → zero ≤ n
          ls : (m n : ℕ) → m ≤ n → suc m ≤ suc n

        ≤-antisym : (m n : ℕ) → m ≤ n → n ≤ m → m ≡ n
        ≤-antisym .zero    .zero    (lz .zero) (lz .zero)   = refl
        ≤-antisym .(suc m) .(suc n) (ls m n p) (ls .n .m q) =
                     cong suc (≤-antisym m n p q)

    * [ Issue 1025 ]

        postulate mySpace : Set
        postulate myPoint : mySpace

        data Foo : myPoint ≡ myPoint → Set where
          foo : Foo refl

        test : (i : foo ≡ foo) → i ≡ refl
        test refl = {!!}

      When applying injectivity to the equation “foo ≡ foo” of type “Foo refl”,
      it is checked that the index refl of type “myPoint ≡ myPoint” is
      self-unifiable. The equation “refl ≡ refl” again requires injectivity, so
      now the index myPoint is checked for self-unifiability, hence the error:

        Cannot eliminate reflexive equation myPoint = myPoint of type
        mySpace because K has been disabled.
        when checking that the pattern refl has type foo ≡ foo

  Termination checking

  * A buggy facility coined “matrix-shaped orders” that supported
    uncurried functions (which take tuples of arguments instead of one
    argument after another) has been removed from the termination
    checker. [Issue 787]

  * Definitions which fail the termination checker are not unfolded any
    longer to avoid loops or stack overflows in Agda.  However, the
    termination checker for a mutual block is only invoked after
    type-checking, so there can still be loops if you define a
    non-terminating function.  But termination checking now happens
    before the other supplementary checks: positivity, polarity,
    injectivity and projection-likeness.
    Note that with the pragma {-# NO_TERMINATION_CHECK #-} you can make
    Agda treat any function as terminating.

  * Termination checking of functions defined by ‘with’ has been improved.

    Cases which previously required —termination-depth
    to pass the termination checker (due to use of ‘with’) no longer
    need the flag. For example

      merge : List A → List A → List A
      merge [] ys = ys
      merge xs [] = xs
      merge (x ∷ xs) (y ∷ ys) with x ≤ y
      merge (x ∷ xs) (y ∷ ys)    | false = y ∷ merge (x ∷ xs) ys
      merge (x ∷ xs) (y ∷ ys)    | true  = x ∷ merge xs (y ∷ ys)

    This failed to termination check previously, since the ‘with’ expands to an
    auxiliary function merge-aux:

      merge-aux x y xs ys false = y ∷ merge (x ∷ xs) ys
      merge-aux x y xs ys true  = x ∷ merge xs (y ∷ ys)

    This function makes a call to merge in which the size of one of the arguments
    is increasing. To make this pass the termination checker now inlines the
    definition of merge-aux before checking, thus effectively termination
    checking the original source program.

    As a result of this transformation doing ‘with’ on a variable no longer
    preserves termination. For instance, this does not termination check:

      bad : Nat → Nat
      bad n with n
      … | zero  = zero
      … | suc m = bad m

  * The performance of the termination checker has been improved.  For
    higher —termination-depth the improvement is significant.
    While the default —termination-depth is still 1, checking with
    higher —termination-depth should now be feasible.

  Compiler backends

  * The MAlonzo compiler backend now has support for compiling modules
    that are not full programs (i.e. don’t have a main function). The
    goal is that you can write part of a program in Agda and the rest in
    Haskell, and invoke the Agda functions from the Haskell code. The
    following features were added for this reason:

    * A new command-line option —compile-no-main: the command

        agda —compile-no-main Test.agda

      will compile Test.agda and all its dependencies to Haskell and
      compile the resulting Haskell files with —make, but (unlike
      —compile) not tell GHC to treat Test.hs as the main module. This
      type of compilation can be invoked from emacs by customizing the
      agda2-backend variable to value MAlonzoNoMain and then calling
      “C-c C-x C-c” as before.

    * A new pragma COMPILED_EXPORT was added as part of the MAlonzo FFI.
      If we have an agda file containing the following:

         module A.B where

         test : SomeType
         test = someImplementation

         {-# COMPILED_EXPORT test someHaskellId #-}

      then test will be compiled to a Haskell function called
      someHaskellId in module MAlonzo.Code.A.B that can be invoked from
      other Haskell code. Its type will be translated according to the
      normal MAlonzo rules.


  Emacs mode

  * A new goal command “Helper Function Type” (C-c C-h) has been added.

    If you write an application of an undefined function in a goal, the Helper
    Function Type command will print the type that the function needs to have in
    order for it to fit the goal. The type is also added to the Emacs kill-ring
    and can be pasted into the buffer using C-y.

    The application must be of the form “f args” where f is the name of the
    helper function you want to create. The arguments can use all the normal
    features like named implicits or instance arguments.


      Here’s a start on a naive reverse on vectors:

        reverse : ∀ {A n} → Vec A n → Vec A n
        reverse [] = []
        reverse (x ∷ xs) = {!snoc (reverse xs) x!}

      Calling C-c C-h in the goal prints

        snoc : ∀ Ā {n} → Vec A n → A → Vec A (suc n)

  * A new command “Explain why a particular name is in scope” (C-c C-w) has been
    added. [Issue207]

    This command can be called from a goal or from the top-level and will as the
    name suggests explain why a particular name is in scope.

    For each definition or module that the given name can refer to a trace is
    printed of all open statements and module applications leading back to the
    original definition of the name.

    For example, given

      module A (X : Set₁) where
        data Foo : Set where
          mkFoo : Foo
      module B (Y : Set₁) where
        open A Y public
      module C = B Set
      open C

    Calling C-c C-w on mkFoo at the top-level prints

      mkFoo is in scope as
      * a constructor Issue207.C._.Foo.mkFoo brought into scope by
        - the opening of C at Issue207.agda:13,6–7
        - the application of B at Issue207.agda:11,12–13
        - the application of A at Issue207.agda:9,8–9
        - its definition at Issue207.agda:6,5–10

    This command is useful if Agda complains about an ambiguous name and you need
    to figure out how to hide the undesired interpretations.

  * Improvements to the “make case” command (C-c C-c)

    - One can now also split on hidden variables, using the name
      (starting with .) with which they are printed.
      Use C-c C-, to see all variables in context.

    - Concerning the printing of generated clauses:

    * Uses named implicit arguments to improve readability.

    * Picks explicit occurrences over implicit ones when there is a choice of
      binding site for a variable.

    * Avoids binding variables in implicit positions by replacing dot patterns
      that uses them by wildcards (._).

  * Key bindings for lots of “mathematical” characters (examples: 𝐴𝑨𝒜𝓐𝔄)
    have been added to the Agda input method.
    Example: type \MiA\MIA\McA\MCA\MfA to get 𝐴𝑨𝒜𝓐𝔄.

    Note: \McB does not exist in unicode (as well as others in that style),
    but the \MC (bold) alphabet is complete.

  * Key bindings for “blackboard bold” B (𝔹) and 0–9 (𝟘-𝟡) have been added
    to the Agda input method (\bb and \b[0–9]).

  * Key bindings for controlling simplification/normalisation:

    [TODO: Simplification should be explained somewhere.]

    Commands like “Goal type and context” (C-cC-,) could previously be
    invoked in two ways. By default the output was normalised, but if a
    prefix argument was used (for instance via C-uC-cC-,), then no
    explicit normalisation was performed. Now there are three options:

    * By default (C-cC-,) the output is simplified.

    * If C-u is used exactly once (C-uC-cC-,), then the result is
      neither (explicitly) normalised nor simplified.

    * If C-u is used twice (C-uC-uC-cC-,), then the result is

    [TODO: As part of the release of Agda 2.3.4 the key binding page on
    the wiki should be updated.]


  * Two new color scheme options were added to agda.sty:

    \usepackage[bw]{agda}, which highlights in black and white;
    \usepackage[conor]{agda}, which highlights using Conor’s colors.

    The default (no options passed) is to use the standard colors.

  * If agda.sty cannot be found by the latex environment, it is now
    copied into the latex output directory (‘latex’ by default) instead
    of the working directory. This means that the commands needed to
    produce a PDF now is

      agda —latex -i . <file>.lagda
      cd latex
      pdflatex <file>.tex

  * The LaTeX-backend has been made more tool agnostic, in particular
    XeLaTeX and LuaLaTeX should now work. Here is a small example


      data αβγδεζθικλμνξρστυφχψω : Set₁ where

        →⇒⇛⇉⇄↦⇨↠⇀⇁ : Set

      ∀X [ ∅ ∉ X ⇒ ∃f:X ⟶  ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]

    Compiled as follows, it should produce a nice looking PDF (tested with
    TeX Live 2012):

      agda —latex <file>.lagda
      cd latex
      xelatex <file>.tex (or lualatex <file>.tex)

    If symbols are missing or xelatex/lualatex complains about the font
    missing, try setting a different font using:


    Use the fc-list tool to list available fonts.

  * Add experimental support for hyperlinks to identifiers

    If the hyperref latex package is loaded before the agda package and
    the links option is passed to the agda package, then the agda package
    provides a function called \AgdaTarget. Identifiers which have been
    declared targets, by the user, will become clickable hyperlinks in the
    rest of the document. Here is a small example


      data ℕ : Set where
        zero  : ℕ
        suc   : ℕ → ℕ

      See next page for how to define \AgdaFunction{two} (doesn’t turn into a
      link because the target hasn’t been defined yet). We could do it
      manually though; \hyperlink{two}{\AgdaDatatype{two}}.


      two : ℕ
      two = suc (suc zero)

      \AgdaInductiveConstructor{zero} is of type
      \AgdaDatatype{ℕ}. \AgdaInductiveConstructor{suc} has not been defined to
      be a target so it doesn’t turn into a link.


      Now that the target for \AgdaFunction{two} has been defined the link
      works automatically.

      data Bool : Set where
        true false : Bool

      The AgdaTarget command takes a list as input, enabling several
      targets to be specified as follows:

      \AgdaTarget{if, then, else, if\_then\_else\_}
      if_then_else_ : {A : Set} → Bool → A → A → A
      if true  then t else f = t
      if false then t else f = f


      Mixfix identifier need their underscores escaped:


    The boarders around the links can be suppressed using hyperref’s
    hidelinks option:


    Note that the current approach to links does not keep track of scoping
    or types, and hence overloaded names might create links which point to
    the wrong place. Therefore it is recommended to not overload names
    when using the links option at the moment, this might get fixed in the