Update src/real-numbers/rational-real-numbers.lagda.md

Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Feb 24, 2024 · 599a4d0 · 599a4d0
1 parent a0e19c3
commit 599a4d0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md
@@ -93,7 +93,7 @@ real-rational x =
     ( is-dedekind-cut-le-ℚ x)
 ```
 
-### The rational real property
+### The property of being a rational real number
 
 ```agda
 module _