michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(doc/lean/library_style.org): clarify C_of_A_of_B convention

Browse source
This commit is contained in:
Jeremy Avigad 2015-12-31 12:59:31 -08:00 committed by Leonardo de Moura
parent 7f25dd6646
commit e14a2aaf3c
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/lean/library_style.org
View file

@ -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=.