coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] bottom , false

From: Patricia Peratto <psperatto AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] bottom , false
Date: Mon, 20 Apr 2020 22:21:01 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=psperatto AT gmail.com; spf=Pass smtp.mailfrom=psperatto AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f181.google.com
Ironport-phdr: 9a23:leSExh9LdgzTOv9uRHKM819IXTAuvvDOBiVQ1KB40uscTK2v8tzYMVDF4r011RmVBNidt64P17OempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgVFiCCybL59Ixm7ohjdvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh/27ZisJ+gqFGrhy/uxNy2JTbbJ2POfdkYq/RYdEXSGxcVchRTSxBBYa8YpMVAeUbIeZYtYj9qEcPrRSkGAKiHv3gyiVSiX/qwa061PkqHAbe3Aw7B9IBrm7Uo8/pNKcOVuC416bIzTDZYPNX3Tfx8pTHchckofyVW797bMnfyVE3Gg/bklmdrZbpMjCV2+gXrWSX8u5tWfiyh2Mktg18pCWkyN02hYnTnI0Vz0jJ9SVnz4YxIt21UEt7bsSlEJtUri2bN5B5Tt47T2FmpSo3yaAKtYS0fCgNz5QnyBrfZOKdf4eU5RLjUf6dITZ+hH17ZLKynwi+/VSkx+HmVcS50ExGojRYntTIrHwByh/e5tWfRvt45Eih2DKP1w7J6uFDJEA5jbLbK4U5wrEujJocq1jDHjPxmEjtg6+Wc18r+ums6+j9frrmoZqcO5duig7iKqQuhtC/AeMgPwcSWGib4P2w26Hn/U3kW7pHleY2k6ncsJDCP8sXvK+5AwlP0oYi8RmzFTmm0M5L1UUAeVlCYVeMi5XjE1DIOvHxS/ml0Hq2lzI+//naJLzqA5yFFnXZmav9ev4p81VExRA60cxYz51RA7AFZvn0Xxmi55TjEhYlPlnskK7cA9Jn29ZGAD7dMuqiKKrX9GSwyKc3OeDVPd0avT/8L74u4Pu81SZky29YRrGg2N4sUF79HvliJB/HM3/lg9NEAG1T+wRnHLWsh1qFXjpeIX21WvBkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkfWF+JGHbsMY6DXqVVZQ==

There is a problema with overloading.

bottom in english is floor.

I interpret perp as perpendicular.

The symbol is perpendicular and in type theory

means false.

We are saying our floor is false?

Regards,

Patricia

[Coq-Club] bottom , false, Patricia Peratto, 04/21/2020