From 24c443786d912be47d5b069930c459d442cdbe4e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Sep 2023 13:56:28 +0200
Subject: [PATCH] Document convention to use `f_as_g` in naming.

See https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/459#note_96622
---
 docs/style_guide.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/docs/style_guide.md b/docs/style_guide.md
index d0279d249..492ece945 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -235,6 +235,7 @@ theories/base_logic/lib is for constructions in the base logic (using own)
     M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
     ```
 * Monotonicity lemmas where the relation can be ambiguous are called `<f>_<relation>_mono`, e.g. `Some_included_mono`.
+* For lemmas `f x = g ...` that give a definition of function `f` in terms of `g`, we use `f_as_g`. For example, `map_compose_as_omap : m ∘ₘ n = omap (m !!.) n`.
 
 ### Naming algebra libraries
 
-- 
GitLab