From e14a2aaf3ca0da173dbf808c43176b640235ee49 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 31 Dec 2015 12:59:31 -0800
Subject: [PATCH] feat(doc/lean/library_style.org): clarify C_of_A_of_B
 convention

---
 doc/lean/library_style.org | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/doc/lean/library_style.org b/doc/lean/library_style.org
index 1acf49001f..f3d95a3176 100644
--- a/doc/lean/library_style.org
+++ b/doc/lean/library_style.org
@@ -77,6 +77,10 @@ check lt_of_not_ge
 check lt_of_le_of_ne
 check add_lt_add_of_lt_of_le
 #+END_SRC
+The hypotheses are listed in the order they appear, /not/ reverse
+order. For example, the theorem =A → B → C= would be named
+=C_of_A_of_B=.
+
 Sometimes abbreviations or alternative descriptions are easier to work
 with. For example, we use =pos=, =neg=, =nonpos=, =nonneg= rather than
 =zero_lt=, =lt_zero=, =le_zero=, and =zero_le=.