[Agda] ANNOUNCE: Agda 2.2.4
Nils Anders Danielsson
nad at Cs.Nott.AC.UK
Tue Jul 7 23:50:28 CEST 2009
Hi,
Agda 2.2.4 has now been released. Important changes since 2.2.2:
* Change to the semantics of "open import" and "open module". The
declaration
open import M <using/hiding/renaming>
now translates to
import A
open A <using/hiding/renaming>
instead of
import A <using/hiding/renaming>
open A.
The same translation is used for "open module M = E …". Declarations
involving the keywords as or public are changed in a corresponding
way ("as" always goes with import, and "public" always with open).
This change means that import directives do not affect the qualified
names when open import/module is used. To get the old behaviour you
can use the expanded version above.
* Names opened publicly in parameterised modules no longer inherit the
module parameters. Example:
module A where
postulate X : Set
module B (Y : Set) where
open A public
In Agda 2.2.2 B.X has type (Y : Set) → Set, whereas in Agda 2.2.4
B.X has type Set.
* Previously it was not possible to export a given constructor name
through two different "open public" statements in the same module.
This is now possible.
* Unicode subscript digits are now allowed for the hierarchy of
universes (Set₀, Set₁, …): Set₁ is equivalent to Set1.
--
/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.
More information about the Agda
mailing list