Skip to content

Commit

Permalink
Fix broken links in MIXFIX-OPERATORS.md (#859)
Browse files Browse the repository at this point in the history
The links in MIXFIX-OPERATORS led to the 404 page on readthedocs. This
PR fixes them.
  • Loading branch information
EgbertRijke authored Oct 18, 2023
1 parent 921edf1 commit 0242199
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
2 changes: 1 addition & 1 deletion CODINGSTYLE.md
Original file line number Diff line number Diff line change
Expand Up @@ -284,7 +284,7 @@ the `agda-unimath` library:
need to sort them by hand.

- The library doesn't use
[variables](https://agda.readthedocs.io/en/v2.6.3/language/generalization-of-declared-variables.html)
[variables](https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html)
at the moment. All variables are declared either as parameters of an anonymous
module or in the type specification of a construction.

Expand Down
6 changes: 3 additions & 3 deletions MIXFIX-OPERATORS.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

This document outlines our choices of conventions for setting precedence levels
and associativity of
[mixfix operators in Agda](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html),
[mixfix operators in Agda](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html),
and provides guidelines for this.

## Mixfix operators in Agda
Expand All @@ -16,7 +16,7 @@ and mixfix operators in Agda is to make the code more readable by using commonly
accepted notation for widely used operators.

Mixfix operators can each be assigned a
[precedence level](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#precedence).
[precedence level](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#precedence).
This can in principle be any signed fractional value, although we prefer them to
be non-negative integral values. The higher this value is, the higher precedence
the operator has, meaning it is evaluated before operators with lower
Expand All @@ -32,7 +32,7 @@ is parsed as `x +ℕ (y *ℕ z)`.

In addition to a precedence level, every mixfix operator can be defined to be
either left or right
[associative](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#associativity).
[associative](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#associativity).
It can be beneficial to define associativity of operators, to avoid excessively
parenthesized expressions. The parenthization should, however, never be omitted
when this can make the code more ambiguous or harder to read.
Expand Down

0 comments on commit 0242199

Please sign in to comment.