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 20:09:48 -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> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1427674242 19064 80.91.229.3 (30 Mar 2015 00:10:42 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 30 Mar 2015 00:10:42 +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 02:10:33 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 1YcNHk-0000v2-GF for geh-help-gnu-emacs@m.gmane.org; Mon, 30 Mar 2015 02:10:32 +0200 Original-Received: from localhost ([::1]:58670 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcNHj-0001Nn-BS for geh-help-gnu-emacs@m.gmane.org; Sun, 29 Mar 2015 20:10:31 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:49853) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcNHV-0001Nh-EY for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 20:10:18 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1YcNHQ-0000cR-GB for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 20:10:17 -0400 Original-Received: from plane.gmane.org ([80.91.229.3]:59743) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcNHQ-0000cG-AI for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 20:10:12 -0400 Original-Received: from list by plane.gmane.org with local (Exim 4.69) (envelope-from ) id 1YcNHN-0000en-VG for help-gnu-emacs@gnu.org; Mon, 30 Mar 2015 02:10:10 +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 02:10:09 +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 02:10:09 +0200 X-Injected-Via-Gmane: http://gmane.org/ Original-Lines: 28 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:ZLJlsYXALO6U/VwZOmCpssyxhzs= 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:103429 Archived-At: > What is α? What is β? > Wouldn't have it been better to name those variables number-of-rows > or tree-height or some other words denoting their actual meaning? Usually, within the context where the mathematical formula is used, these variables *are* names denoting their meaning. These depend on notational conventions used within specific communities (and usually not formalized), but they are convenient. So instead of has_type env exp type you say Γ ⊢ e : τ and it is just as explicit, because τ does mean "a type", and Γ means "a type environment", and ":" means "has type", and "⊢" means "based on hypotheses such and such". Some of those letters/signs have meaning shared within a fairly large mathematical community while others are much more specific to a specialized subfield. Of course, if you're not familiar with the local conventions, it looks like line noise, but otherwise it offers people much higher concision, so they can focus on the important aspects. Stefan