Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] injectivity of constructors

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity of constructors


Chronological Thread 
  • From: Lily Chung <ikdc AT mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] injectivity of constructors
  • Date: Thu, 13 Dec 2018 19:53:34 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ikdc AT mit.edu; spf=Pass smtp.mailfrom=ikdc AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-2.mit.edu
  • Importance: Normal
  • Ironport-phdr: 9a23:dzYm/hJsA8Yes7mHQtmcpTZWNBhigK39O0sv0rFitYgQLfXxwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhikaOTA68m7ZitJ+g6FBrh2gqBNw34HabZqVNPVlZK7RYc8WSXZDU8tXSidPApm8b4wKD+cZO+hYro39plsTphagBQmsGeXvyjBVjXLx3K060PkuHh3d0QwlHtIOrG7Yo8voO6cPSO24yrTDwzbbb/5OxDvw65LEfxQ7rf2SXb98a9fdxEc3Gw/YjFict5bpMjOU2+gXrWSW4fBsWOKhhmMhtgp/uCKgxt02hYnMno8Vyk7L9SF+wIstONK4TU96bcehEJRKtiGaM5B2Td0+TG1xoyY11qcJuZi9fCcU0pQr3gDTZ+aCc4iJ/hLvTvieLiplhH59ebK/gQi98VS4x+HhVcS4ylJHojBbntTMrHwByhLe5tCCSvRn/0eh3TiP1xrU6uFBOU00lKnbJIM9zbMrk5oTsFjDEjXol0rrka+abl8k9fSw6+T7frXmoYeROJNzigHnK6ghhsi/AfkjPQUVRGia+eG81KX58kHjQbVKiOc2kqjDv5zAK8QbvP3xPwgA2YE6rh27Ej2O0dICnHBBIkgWVgiAit3NOlXfaNv4EPGwywCtkztg7/XHIvvsDoibfSuLq6voYbsosx0U8wE0190Kv8sFWIFEG+r6XwrKjPKdCxY4NwKuxOO2WtB8ysUTVX/dW/bFYpOXikeB46cUG8fJfJUc6WT4KuRj6vLz3ydgxA0tOJKx1J5SU0iWW/RrJ0LCOCjgh8VEFG4LuhEzR6nxg1SEVzNJIiz0WqMgoDw3FdD+AA==

That follows from general properties of equality, and has nothing to do with constructors.  Try f_equal.



Archive powered by MHonArc 2.6.18.

Top of Page