coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Understanding Coq Discrimination Trees
- Date: Sun, 29 Mar 2020 16:30:07 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f177.google.com
- Ironport-phdr: 9a23:E2FuvRbo2klQGLfbd8Z4O4r/LSx+4OfEezUN459isYplN5qZr8i/bnLW6fgltlLVR4KTs6sC17OK9fm+AidZvM/JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sArcutMLjYZjJKs9xQbFr3tVd+9L2W5mOFWfkgrz6cu34JNt6Tlbteg7985HX6X6fqA4QqJdAT87LW0759DluAfaQweX6XQSTmsZkhxTAwjY9x76RYv+sjH7tuVmxiaXO9D9QK0uVjSj66drTwLoiDsCOjUk/mzbltB8gaRGqx+6uRdx35Dbb52UNPpmf6PSY9UaRXZaXs1MUyBNG56wY5cTA+YEO+tXqJTzp0YVrRumGwajGP/vxDFPhn/zx6I60uIhGhzC0AEvG98CtXLZp8j3OqgPS+C41KbHwzXNYf1VxDnz9pTHfws7rv2QR799a9bdxVUtGg7Dk16eqZblPzSQ1ukVsmab9fRvVe2oi249qwB6vz+hyd0oiobXmo0VykrL/jh+zYY6IN23Ukp7bsC4H5tQrS6XLIR2QsY4TGFpvCY20KEJuZm+fCUTzpks2hDRa/uCc4eS4xLjUv6cITh5hHJ5eLK/mg29/VKhyu37UMS/zVVErjJdn9XSqnwA0wbf58uHR/dn40us2DSC2xrO5uxGI005k7fQJYQ7zb4qjJUTtFzOHi/ol0Xyi6+bbkAk9fKp6+Tje7nmoZ6cO5JthgHwL6gjmM6yDf43MggJWGib9uC826P58ULlR7VKi+U6kqjfsJ/EOcQWvrC1DxNR34o56BuyDy2q3MkZkHQFNl5JZRCKgorxN1HLOv/4DPO/g1q2kDdswvDLJrLhApDXIXjHjrjuYbZ95FRHxQo8yNBQ/ZNUCrUbLP3vXU/xscTUDgUlPAys3+bnFNJ925sCVmKIG6+VKb/dsVuV5u00OOSMf48UuDPlK/c//fLujHk5mUUcfaazx5cXZmq4TbxaJBCyZmOkqdMcGy9etQ0nCefulVeqUDhJZn/0UbhqtR8hD4fzIp3OSYe3kfSk1SO2FZ1fLjRJD1mIHHzofq2LXv4NbGSZJco3wW9MbqSoV4J0jULmjwT90bcya7eNo3FKhdfYzNFwotbru1Qq7zUtVpaS1miMSyd/mWZaH2ZnjpA6mlR0zxK46YY9hvVZEdJJ4PYQC1U1MJfdy6pxDNWgA1ucLOfMc06vR5CdOR90Tt81xIVQMUN0GtHniRGamiTzXOBTmLuMC5g5tKnb2iqpKg==
Hello --
Sometimes I find that when I run typeclasses eauto it seems like there are a lot of "possibilities" but in fact there are very few that match based on the goal. So I'm wondering, do discrimination trees cut off at some depth? What is done with transparent symbols that unfold to other symbols?
- [Coq-Club] Understanding Coq Discrimination Trees, Gregory Malecha, 03/29/2020
Archive powered by MHonArc 2.6.18.