From 0242199cd09e6f119909b3804fb805c02bc6c352 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 18 Oct 2023 18:16:29 +0200 Subject: [PATCH] Fix broken links in `MIXFIX-OPERATORS.md` (#859) The links in MIXFIX-OPERATORS led to the 404 page on readthedocs. This PR fixes them. --- CODINGSTYLE.md | 2 +- MIXFIX-OPERATORS.md | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CODINGSTYLE.md b/CODINGSTYLE.md index b02c0b2eb0..6e0d1a3f12 100644 --- a/CODINGSTYLE.md +++ b/CODINGSTYLE.md @@ -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. diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md index e2bc34c8a3..0eb4646cc4 100644 --- a/MIXFIX-OPERATORS.md +++ b/MIXFIX-OPERATORS.md @@ -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 @@ -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 @@ -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.