Changelog for Agda-2.4.2

If this renders badly as markdown, see the plain text version

-- Release notes for Agda version 2.4.2

Important changes since 2.4.0.2:

Pragmas and options

Language

Type checking

Tools

Emacs mode

LaTeX-backend


-- Release notes for Agda 2 version 2.4.0.2

Important changes since 2.4.0.1:


-- Release notes for Agda 2 version 2.4.0.1

Important changes since 2.4.0:


-- Release notes for Agda 2 version 2.4.0

Important changes since 2.3.2.2:

Installation and infrastructure

Pragmas and options

Language

-- 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:

Goal and error display

Type checking

Termination checking

Compiler backends

Tools

Emacs mode

LaTeX-backend


-- Release notes for Agda 2 version 2.3.2.2

Important changes since 2.3.2.1:


-- Release notes for Agda 2 version 2.3.2.1

Important changes since 2.3.2:

Installation

Type checking


-- Release notes for Agda 2 version 2.3.2

Important changes since 2.3.0:

Installation

Pragmas and options

Language

Goal and error display

Type checking

Compiler backends

Tools

Emacs mode

LaTeX-backend

An experimental LaTeX-backend which does precise highlighting a la the HTML-backend and code alignment a la lhs2TeX has been added.

Here is a sample input literate Agda file:

\documentclass{article}

\usepackage{agda}

\begin{document}

The following module declaration will be hidden in the output.

\AgdaHide{ \begin{code} module M where \end{code} }

Two or more spaces can be used to make the backend align stuff.

\begin{code} data ℕ : Set where zero : ℕ suc : ℕ → ℕ

+ : ℕ → ℕ → ℕ zero + n = n suc m + n = suc (m + n) \end{code}

\end{document}

To produce an output PDF issue the following commands:

agda --latex -i . <file>.lagda pdflatex latex/<file>.tex

Only the top-most module is processed, like with lhs2tex and unlike with the HTML-backend. If you want to process imported modules you have to call agda --latex manually on each of those modules.

There are still issues related to formatting, see the bug tracker for more information:

https://code.google.com/p/agda/issues/detail?id=697

The default agda.sty might therefore change in backwards-incompatible ways, as work proceeds in trying to resolve those problems.

Implemented features:


-- Release notes for Agda 2 version 2.3.0

Important changes since 2.2.10:

Language

Universe polymorphism

Meta-variables and unification

Irrelevance

Reflection

Compiler backends

MAlonzo

Epic

JavaScript

Tools


-- Release notes for Agda 2 version 2.2.10

Important changes since 2.2.8:

Language

Tools


-- Release notes for Agda 2 version 2.2.8

Important changes since 2.2.6:

Language

Tools


-- Release notes for Agda 2 version 2.2.6

Important changes since 2.2.4:

Language

Tools


-- Release notes for Agda 2 version 2.2.4

Important changes since 2.2.2:


-- Release notes for Agda 2 version 2.2.2

Important changes since 2.2.0:

Tools

Infrastructure


-- Release notes for Agda 2 version 2.2.0

Important changes since 2.1.2 (which was released 2007-08-16):

Language

Tools

Libraries

Documentation

Infrastructure