Skip to Content.
Sympa Menu

coq-club - [Coq-Club] consistency

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] consistency


Chronological Thread 
  • From: Patricia Peratto <psperatto AT vera.com.uy>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] consistency
  • Date: Sat, 1 Feb 2020 21:16:55 -0300 (UYT)
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
  • Dkim-filter: OpenDKIM Filter v2.9.0 mta02.in.vera.com.uy 958B5222212
  • Ironport-phdr: 9a23:SlW/qxM+E3K2mWvBF4Ml6mtUPXoX/o7sNwtQ0KIMzox0Lfv9rarrMEGX3/hxlliBBdydt6sYzbaN+Pm/ESxYuNDd6StEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQZjId4Jas8xBTFrmZKdu9LwW9kOU+fkwzz68ut8pNv6Thct+4k+8VdTaj0YqM0QKBCAj87KW41/srrtRfCTQuL+HQRV3gdnwRLDQbY8hz0R4/9vSTmuOVz3imaJtD2QqsvWTu+9adrSQTnhzkBOjUk7WzYkM1wjKZcoBK8uxxyxpPfbY+JOPZieK7WYNUXTndDUMlMTSxMGo2yYYsRAeQCP+lWsobyqEcPrRuiHgSjHv/jxSNTiXPqwaE30eIsGhzG0gw6GNIOtWzZos/vO6cOS+C1zbXHzTTZYPhLwzny9pLIfQo9ofGQWrJ7bM3cyVE0FwPdkFqQs5bqPy+J1uQKqGWb8fRvVfi1hGI9tw5xpT2vyt0xiojJn48YzE3P+yZhwIstO9G0VFJ3bcSrHZdMrS2XOZZ6Ttk/T2xnoCo2178LtYChcCQUx5kr3RDSZ+Gdf4WG/x7uUvuaLy1ii3J/Yr2/gg6/8Ui+xe34Ucm5yFNKoTBEktnIrHwNyQLc6tKdRfdn4kih3jOP2xrO6uBEOUw0lKzbJIA9wrMoiJYfrVjPEjX5lUnqlqObeFgo9vK15+noernmo4WTN45wigHwKKQuncm/DPwgMggVR2iU5/6826f//U3lR7VHleM2nbfDsJ/AP8gUuqm5AwpP3oY+6xezFy2m38gAnXkbMFJFfwqKgJTuO1HXOfz3EfO/g0m3nzpw3PDHPrjhAo3XIXTZkbfhe6x9609GxwYpw9Bf/cEcNrZUK/XqH0T1qdaQWhQ+Kkm/x/vtINR7zIIXH2yVVPy3KqTX5GeB+vguKOiFLLcYoj/hN/9ts+b1lXIjkEMBeoG30IEeLnu/G7J7MhPKMjLXnt4dHDJS7UIFR+vwhQjaCGIBVzOJR6s5owoDJse+F46aHdKzjaaImiy8G9tLdzIeUwHeITLTb4yBHsw0RmeXK85lnCYDUOH6GZEszxjovwj/jad2fLONp38o8Kn73d0w3NX90BE/8TstX5aY2mCJCX95hGpOTDgzmr1u8xRw

Can not be defined that different constructors are 
different terms automatically?

To not use bottom to prove 0<>1.
To be consistent.

Regards,
Patricia Peratto



Archive powered by MHonArc 2.6.18.

Top of Page