From 086f5b621cf39c5c1b469ba0bca88f885e252986 Mon Sep 17 00:00:00 2001 From: ia0 Date: Thu, 14 Aug 2025 21:25:48 +0200 Subject: [PATCH] Fix typo in resource algebra module --- exercises/resource_algebra.v | 2 +- theories/resource_algebra.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/exercises/resource_algebra.v b/exercises/resource_algebra.v index 3604ac7..99456f2 100644 --- a/exercises/resource_algebra.v +++ b/exercises/resource_algebra.v @@ -30,7 +30,7 @@ From iris.heap_lang Require Import lang proofmode notation. A small side note: in Iris, resource algebras are specialisations of the more general structure `CMRA' (in particular, resource algebras are `discrete' CMRAs). In turn, CMRAs are built on top of `Ordered - Families of Equations' (shortened to `OFE'). The exact details of + Families of Equivalences' (shortened to `OFE'). The exact details of these concepts are not important for this chapter, but we mention them as they appear a few times throughout the chapter. CMRAs and OFEs are covered in more detail in later chapters. diff --git a/theories/resource_algebra.v b/theories/resource_algebra.v index cdfff87..e92c5fb 100644 --- a/theories/resource_algebra.v +++ b/theories/resource_algebra.v @@ -30,7 +30,7 @@ From iris.heap_lang Require Import lang proofmode notation. A small side note: in Iris, resource algebras are specialisations of the more general structure `CMRA' (in particular, resource algebras are `discrete' CMRAs). In turn, CMRAs are built on top of `Ordered - Families of Equations' (shortened to `OFE'). The exact details of + Families of Equivalences' (shortened to `OFE'). The exact details of these concepts are not important for this chapter, but we mention them as they appear a few times throughout the chapter. CMRAs and OFEs are covered in more detail in later chapters.