From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Stefan Monnier Newsgroups: gmane.emacs.help Subject: Re: if vs. when vs. and: style question Date: Sun, 29 Mar 2015 21:50:58 -0400 Message-ID: References: <87sicvwckx.fsf@wmi.amu.edu.pl> <87wq27yvqg.fsf@debian.uxu> <8d531e99-7260-4263-ac99-09c6871e2708@googlegroups.com> <87vbhq53lf.fsf@debian.uxu> <87a8z23p23.fsf@kuiper.lan.informatimago.com> <87lhilx0cf.fsf@debian.uxu> <87twx9360u.fsf@kuiper.lan.informatimago.com> <0d1d19ab-06e9-462d-8867-9a49b1e232d3@googlegroups.com> <87pp7x2jav.fsf@kuiper.lan.informatimago.com> <87d23s4nt4.fsf@debian.uxu> <7e8ddf8f-163a-4d16-9ce2-25b0cb3f35aa@googlegroups.com> <87sicny7zm.fsf@kuiper.lan.informatimago.com> <874mp3clqi.fsf@wanadoo.es> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain X-Trace: ger.gmane.org 1427680305 6933 80.91.229.3 (30 Mar 2015 01:51:45 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 30 Mar 2015 01:51:45 +0000 (UTC) To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Mon Mar 30 03:51:41 2015 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1YcOrc-00026B-Gn for geh-help-gnu-emacs@m.gmane.org; Mon, 30 Mar 2015 03:51:40 +0200 Original-Received: from localhost ([::1]:58920 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcOrb-0001uj-L8 for geh-help-gnu-emacs@m.gmane.org; Sun, 29 Mar 2015 21:51:39 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:39043) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcOrQ-0001ue-PO for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 21:51:29 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1YcOrN-0004OJ-Jp for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 21:51:28 -0400 Original-Received: from plane.gmane.org ([80.91.229.3]:34834) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcOrN-0004OE-DF for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 21:51:25 -0400 Original-Received: from list by plane.gmane.org with local (Exim 4.69) (envelope-from ) id 1YcOrJ-0001sk-9Z for help-gnu-emacs@gnu.org; Mon, 30 Mar 2015 03:51:21 +0200 Original-Received: from 65-110-216-75.cpe.pppoe.ca ([65.110.216.75]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Mar 2015 03:51:21 +0200 Original-Received: from monnier by 65-110-216-75.cpe.pppoe.ca with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Mar 2015 03:51:21 +0200 X-Injected-Via-Gmane: http://gmane.org/ Original-Lines: 13 Original-X-Complaints-To: usenet@ger.gmane.org X-Gmane-NNTP-Posting-Host: 65-110-216-75.cpe.pppoe.ca User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.0.50 (gnu/linux) Cancel-Lock: sha1:b6pVAaXtTG6MZxQYzTgBSxhErCg= X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 80.91.229.3 X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Xref: news.gmane.org gmane.emacs.help:103432 Archived-At: > Those conventions make sense when you work on the same field for long > enough periods (students, specialized programmers...) but I guess that > most of us deal with heterogeneous code on a regular basis. Heck, we do I was talking about math, not code. Of course, in cases like Coq and Agda, the overlap between the two can be significant, so there's a commensurately strong pressure to make sure the code follows the same notation as the math, to make it easier to relate the two (which is often crucial, since the code is the one that's mechanically checked to convince one that the math is right). Stefan