Skip to content

Commit

Permalink
[ agda#6055, CHANGELOG ] latest -> v20221128.
Browse files Browse the repository at this point in the history
  • Loading branch information
asr committed Nov 28, 2022
1 parent 85e798f commit 22d4978
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Highlights
----------

* Added support for [Erased Cubical
Agda](https://agda.readthedocs.io/en/latest/language/cubical.html#cubical-agda-with-erased-glue),
Agda](https://agda.readthedocs.io/en/v2.6.2.2.20221128/language/cubical.html#cubical-agda-with-erased-glue),
a variant of Cubical Agda that is supported by the GHC backend,
under the flag `--erased-cubical`.

Expand All @@ -15,7 +15,7 @@ Highlights

Since `--cubical-compatible` mode implies that functions should work
with the preliminary support for [indexed inductive types in Cubical
Agda](https://agda.readthedocs.io/en/latest/language/cubical.html#indexed-inductive-types),
Agda](https://agda.readthedocs.io/en/v2.6.2.2.20221128/language/cubical.html#indexed-inductive-types),
many pattern matching functions will now emit an
`UnsupportedIndexedMatch` warning, indicating that the function will
not compute when applied to transports (from `--cubical` code).
Expand All @@ -28,7 +28,7 @@ Highlights

* New primitives `declareData`, `defineData`, and `unquoteDecl data`
for generating new data types have been added to the [reflection
API](https://agda.readthedocs.io/en/latest/language/reflection.html#metaprogramming).
API](https://agda.readthedocs.io/en/v2.6.2.2.20221128/language/reflection.html#metaprogramming).

* Thanks to a number of performance improvements, Agda 2.6.3 is about
30% faster than Agda 2.6.2.2 at type-checking the standard library
Expand All @@ -52,7 +52,7 @@ Erasure
regular Cubical Agda code from this variant of Cubical Agda, but
names defined using Cubical Agda are (mostly) treated as if they had
been marked as erased. See the [reference
manual](https://agda.readthedocs.io/en/latest/language/cubical.html#cubical-agda-with-erased-glue-and-erased-higher-constructors)
manual](https://agda.readthedocs.io/en/v2.6.2.2.20221128/language/cubical.html#cubical-agda-with-erased-glue-and-erased-higher-constructors)
for more details.

The GHC backend can compile code that uses `--erased-cubical` if the
Expand Down Expand Up @@ -121,7 +121,7 @@ Cubical Agda

* Cubical Agda now has experimental support for indexed inductive types
([#3733](https://github.com/agda/agda/issues/3733)).
See the [user guide](https://agda.readthedocs.io/en/latest/language/cubical.html#indexed-inductive-types)
See the [user guide](https://agda.readthedocs.io/en/v2.6.2.2.20221128/language/cubical.html#indexed-inductive-types)
for caveats.

* The cubical interval `I` now belongs to its own sort, `IUniv`, rather
Expand Down Expand Up @@ -404,7 +404,7 @@ Library management
Interaction
-----------

* Agsy ([automatic proof search](https://agda.readthedocs.io/en/latest/tools/auto.html)) can
* Agsy ([automatic proof search](https://agda.readthedocs.io/en/v2.6.2.2.20221128/tools/auto.html)) can
now be invoked in the right-hand-sides of copattern matching clauses.
([#5827](https://github.com/agda/agda/pull/5827))

Expand Down

0 comments on commit 22d4978

Please sign in to comment.