Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Understanding Coq Discrimination Trees

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Understanding Coq Discrimination Trees


Chronological Thread 
  • 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?

Any pointers would be greatly appreciated. Thanks.

--
gregory malecha


  • [Coq-Club] Understanding Coq Discrimination Trees, Gregory Malecha, 03/29/2020

Archive powered by MHonArc 2.6.18.

Top of Page