From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Arthur Miller Newsgroups: gmane.emacs.help Subject: Re: [OFFTOPIC] Re: Appending lists Date: Thu, 17 Jun 2021 08:09:08 +0200 Message-ID: References: <4tl1yvylvg1fxx5eefjs9mnk.1623688568572@email.android.com> <87o8c8l32h.fsf@posteo.net> <87zgvs2bup.fsf@zoho.eu> <87y2bby1kr.fsf@zoho.eu> <20210615091834.GB24886@tuxteam.de> <87im2ewr3k.fsf@zoho.eu> <20210616072819.GB17919@tuxteam.de> <20210616151101.GB5669@tuxteam.de> <875yydtnqz.fsf@zoho.eu> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="13755"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (gnu/linux) Cc: Stefan Monnier To: Stefan Monnier via Users list for the GNU Emacs text editor Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane-mx.org@gnu.org Thu Jun 17 08:24:46 2021 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1ltlSG-0003Of-Dm for geh-help-gnu-emacs@m.gmane-mx.org; Thu, 17 Jun 2021 08:24:45 +0200 Original-Received: from localhost ([::1]:33852 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ltlSF-0003kT-7f for geh-help-gnu-emacs@m.gmane-mx.org; Thu, 17 Jun 2021 02:24:43 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:43332) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1ltlRp-0003kL-2F for help-gnu-emacs@gnu.org; Thu, 17 Jun 2021 02:24:17 -0400 Original-Received: from mail-oln040092070076.outbound.protection.outlook.com ([40.92.70.76]:47110 helo=EUR03-AM5-obe.outbound.protection.outlook.com) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1ltlRm-0004ZE-N1 for help-gnu-emacs@gnu.org; Thu, 17 Jun 2021 02:24:16 -0400 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=hOWh7+VBAOoIFKEUdN92lHduWFhXTuFge1dh9lWHJTBfF969Yj3EZUfw9wjscfsRGR9eTx9I9oSpNTkvQ+4Lk0qhu+HbLeVEz12EG/A4HwQ0D9VBbd2/YEVRamMXlNJ66ezm8mEZzeueuTxMGfdNy19IMFaxlBRzzyRNT03jb5JyaGGpHVEl1TJj98yR4dnZbBunb2PyO2gLEzuXYf0nLCK9t/M2YaJzrk2+8UqloIOe072EppRTx55wS7ENjb0z83qftGTmGuXFSs8WbumcaxH4+/4j29jXOAFM2kMnw6P60f/S0uhiV++9eObdlIbhdEkC6956xmyAvLe2zxyeTg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=siQb3VPbyEyQ2ud2O49ZUFTVxsd/b4sK9V2If5YggT8=; b=N5HzzU7BnLLWhTjHr7rnvaO8lO8cftTbEeBNqb3jK3K4kZvrimezW7u8jc337fusldWNB3kV/lf/WstdQaAZ+tZ3BBJ+GEeX4ppRxrohThJZuDKGOEeA0Xwv/BWM7yyZi6Ygh1YEuZKWLkAXxynwKTU6f57g4NH2cy5VAjnqbwzHGxH6Owg1tSIaqU2YdGMS8Q5vv54uAbI/4w2MHcvWPACkyiuMzzTscyuTdvkHxTe/GO6U49POguUgkd7iMcB9cOj7o42FMLxyndXJQ6lj1hoi5eXVaomon6i8AE/cTxfbkouhS37dF71hjdMZaPLYe5ddbYC+thfh5YL0mAsvYA== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=live.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=siQb3VPbyEyQ2ud2O49ZUFTVxsd/b4sK9V2If5YggT8=; b=CoLrbs3bcTPBYrLzKxhJ0aGamM6wclwzOUCsRqB8dpvdLPNwaYEX7Z6tQBFwjrCARyiklJOIkj/B3bStYy0fhBJoLAweqAr61ubs1fx4wHaFrF3sigGPNkznE1W6pA480caYN3/zdNy3gdWI/qqjqKBt9spnciO1g5LNFec1GMZQn+PUl4vjBwuIekN3kOER4m/ud52aTYekMIjdrHSfUvAEjbDCy498m+Z3zHUokaD2Dv2PohHlFIcjj7ZUlGSDU/QIl+Bao1FnoJ7r9eBJpctZyF+y554tjkJnMZHDIEDRoAosUohfh85sTzz0s16POafJlbQ3nuMOSoi1Pg55Yw== Original-Received: from AM5EUR03FT015.eop-EUR03.prod.protection.outlook.com (2a01:111:e400:7e08::45) by AM5EUR03HT129.eop-EUR03.prod.protection.outlook.com (2a01:111:e400:7e08::434) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.4242.16; Thu, 17 Jun 2021 06:09:09 +0000 Original-Received: from AM9PR09MB4977.eurprd09.prod.outlook.com (2a01:111:e400:7e08::42) by AM5EUR03FT015.mail.protection.outlook.com (2a01:111:e400:7e08::132) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.4242.16 via Frontend Transport; Thu, 17 Jun 2021 06:09:09 +0000 X-IncomingTopHeaderMarker: OriginalChecksum:A436A271182B28A776ED4A10D8108A1918E5BB219F962FF1FA8CA3CFCCBE4BA4; UpperCasedChecksum:460F04DB49AF0750E2CF97DB9E25B54E51F552629C460C6DC550F874DF14DC88; SizeAsReceived:7933; Count:46 Original-Received: from AM9PR09MB4977.eurprd09.prod.outlook.com ([fe80::51ca:cb30:2619:5219]) by AM9PR09MB4977.eurprd09.prod.outlook.com ([fe80::51ca:cb30:2619:5219%7]) with mapi id 15.20.4242.019; Thu, 17 Jun 2021 06:09:09 +0000 In-Reply-To: (Stefan Monnier via Users list for the's message of "Wed, 16 Jun 2021 22:41:18 -0400") X-TMN: [8zAAqrlIEOOerUSsrBpKQhRZNpLfGPAD] X-ClientProxiedBy: AM6PR10CA0005.EURPRD10.PROD.OUTLOOK.COM (2603:10a6:209:89::18) To AM9PR09MB4977.eurprd09.prod.outlook.com (2603:10a6:20b:304::20) X-Microsoft-Original-Message-ID: <87bl8510qj.fsf@live.com> X-MS-Exchange-MessageSentRepresentingType: 1 Original-Received: from pascal.homepc (81.232.177.30) by AM6PR10CA0005.EURPRD10.PROD.OUTLOOK.COM (2603:10a6:209:89::18) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.4242.15 via Frontend Transport; Thu, 17 Jun 2021 06:09:08 +0000 X-MS-PublicTrafficType: Email X-IncomingHeaderCount: 46 X-EOPAttributedMessage: 0 X-MS-Office365-Filtering-Correlation-Id: bb9b4019-7b90-44c7-1fd1-08d931566b52 X-MS-TrafficTypeDiagnostic: AM5EUR03HT129: X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: ckJUI0qVMFNyvLjz0vmjj6+0GWEHuxBo97qO35Io1r70DN2Xmqqs3iJsLmgxcwnxfrCgUTOBaCBqsqR+E6QNNVxAUE0BUFpoZKmbLrABQIjknS+xypa5yzQHF+HFkqTF6+9LYGILqjinI/xVsMB7DP2MpYyp8W7VjG81R8bgVl7HHJfqFkjZ5j/7s/fDaeZ4TzJSypeJi+wpeQTtn0LReijX6F4SXPfHMSnLoAcfAFPTtLwMawjxVftX2Y3lNs6LeeTbjlPp7mb+rL/KSjsbL8OrKK1zBchWWyK/KLzlV/pbub4FI82AvH5CWfqp7KDipioPjkF+L+u7kDuPxAtaChHBiBWFgxeiJKFrxVooaPedUZrX6/VxrDEPzRLGCbyiArpJYnc1tILTKcf1okuwbQ== X-MS-Exchange-AntiSpam-MessageData: b0fOpZpOb9xz/Fhpp1Q5/oC2GcRvC0eI2/Zr/IXJoPkrh7msqW843+Loyt9swCM4IV8qFOQpLissJBSSYbP4UcIYSzG3KDGGqoE+jm28EyP/o5R3nGh6KThSMe/rhyWciMCgbjcoOsFK46ZNZvUFLQ== X-OriginatorOrg: live.com X-MS-Exchange-CrossTenant-Network-Message-Id: bb9b4019-7b90-44c7-1fd1-08d931566b52 X-MS-Exchange-CrossTenant-OriginalArrivalTime: 17 Jun 2021 06:09:09.3988 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: 84df9e7f-e9f6-40af-b435-aaaaaaaaaaaa X-MS-Exchange-CrossTenant-AuthSource: AM5EUR03FT015.eop-EUR03.prod.protection.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Anonymous X-MS-Exchange-CrossTenant-FromEntityHeader: Internet X-MS-Exchange-CrossTenant-RMS-PersistedConsumerOrg: 00000000-0000-0000-0000-000000000000 X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM5EUR03HT129 Received-SPF: pass client-ip=40.92.70.76; envelope-from=arthur.miller@live.com; helo=EUR03-AM5-obe.outbound.protection.outlook.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, MSGID_FROM_MTA_HEADER=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_MSPIKE_H2=-0.001, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.23 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-mx.org@gnu.org Original-Sender: "help-gnu-emacs" Xref: news.gmane.io gmane.emacs.help:130951 Archived-At: Stefan Monnier via Users list for the GNU Emacs text editor writes: >>>>> Just to show that you should never say never: >>>> Hey, that's cheating :-) >>> Impredicativity is borderline, indeed. >> Impredicativity, what's that, recursion? > > (with-lecture-mode > > Kind of, except the cycle is not "definition refers to itself" (the > "traditional" form of recursion) but rather "definition can be applied > to itself" as in the first sentence quoted above ;-) > > These forms of circularity have been a great source of hilarity for > logicians and philosophers over the years, but more relevantly for > programmers they've been the source of the invention of the notion of > "type", introduced by Bertrand Russel about a century ago to try and > rule out those forms of circularity by stratifying logical > statements. ) Can you anyhow apply type theory to a definition of time, without refering to time itself? //arthur -- in some philosophical doubts