Skip to content

Commit

Permalink
[ agda#6055, 2.6.3 RC3 ] CHANGELOG: Updated the links to Read the Docs.
Browse files Browse the repository at this point in the history
[ci skip]
  • Loading branch information
asr committed Jan 5, 2023
1 parent 8830b15 commit b0a9a4d
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 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.20230105/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.20230105/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 Down Expand Up @@ -46,7 +46,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.20230105/language/reflection.html#metaprogramming).

Installation and infrastructure
-------------------------------
Expand All @@ -64,7 +64,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.20230105/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 @@ -100,7 +100,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.20230105/language/cubical.html#indexed-inductive-types)
for caveats.

* The cubical interval `I` now belongs to its own sort, `IUniv`, rather
Expand Down Expand Up @@ -306,7 +306,7 @@ Pragmas and options
([#1625](https://github.com/agda/agda/issues/1625)).

Note that use of this option is associated with some potential
[drawbacks](https://agda.readthedocs.io/en/latest/language/lossy-unification.html#drawbacks).
[drawbacks](https://agda.readthedocs.io/en/v2.6.2.2.20230105/language/lossy-unification.html#drawbacks).

* The new option `--no-load-primitives` complements `--no-import-sorts`
by foregoing loading of the primitive modules altogether. This option
Expand Down Expand Up @@ -386,7 +386,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.20230105/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 b0a9a4d

Please sign in to comment.