coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Custom entries examples

From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Custom entries examples
Date: Wed, 31 Jul 2019 09:26:21 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT mx0a-000c2a01.pphosted.com
Ironport-phdr: 9a23:Z2Qo5BFSley24MkFok9LmZ1GYnF86YWxBRYc798ds5kLTJ78oM6wAkXT6L1XgUPTWs2DsrQY0rCQ4v2rBzZIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK1+IA+yoAjRucUbgJVuIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFojKxUvB2vqBNxzYDJY4+bKv1wc7jBfdMDQGpNQsZRWzBDD466coABD/ABPeFdr4TlqVcDsAWxBQ+uBOz1zz9Ih3n21rAk3ug7DArIxg0gEMwUsHvIstr5OroZXOeuw6bU1TXDbu1Z2S3h54fWaR0uvfCMXalqfcrM0UkgCQXFjlOKpYP7IjyVy/0Avm6G5ORjTeKik3Mrpg5yrzS128shi4fEipgIxl3E6Cl12oI4KcOgREN5f9KoCplduiKAO4drXs8uXXtktDg1x7AApJW1ZjIFyI49yB7ac/GHc5aH4hbkVOuJJDd5i25pd6imixqu7USs1vHzWteu31pWsyZJiMHMtmgN1xzU8ciHVuVy8Vq71TmT0ADT7/lIIUEylaXFN54s2qM8m5UQvEjZAyP7mUv7gLWLekgk5+Sk8eDqbqv+qp+ZLYB0iwX+Mqo0msy4BOQ1KhMBUHSD+eS9yrLj51H2T6tRg/Iqk6nZq4rWJdkDpqGnBQ9V1Jwv5AiiADe7yNgYh2UILEpZeBKbiIjkI03BIPfhDfumn1uslCpryOvdM736ApTNK2DDn637cbZ87U5c0gszwspF65JaELFSaM70D0T2rZnTCgIzGw2y2efuTttnha0EXmfaSIWUNqHbtF6Orslpa9GNaZUetXy1f/Iu///jl3Q0sVQcZu+0xZYRbja1EukwcBbRWmblntpUSTRChQE5VuG/0ATTAw4WXG67WucH3h9+DYunCYnZQYX03e6K3Tz9A4VbYGYAB1yRQy6xKte0HswUYSfXGfdP1zwJUb/7G90kxUmn8Veik7E9J7KNvDUAtZX4yNV5oebUkENqrGAmP4Gmy2iIClpMsCYQXTZvgfJ0oFc710+O164+jvBFR4Re

The “custom entries” feature in 8.9 looks extremely cool. Has anyone
developed any significant examples with it that they’d be willing to share?
In particular, has anyone made a grammar for the simply typed lambda-calculus
or some similar system?

Thanks!

- Benjamin

[Coq-Club] Custom entries examples, Benjamin C. Pierce, 07/31/2019
- Re: [Coq-Club] Custom entries examples, Andres Erbsen, 07/31/2019
  - Re: [Coq-Club] Custom entries examples, Emilio Jesús Gallego Arias, 07/31/2019
    - Re: [Coq-Club] Custom entries examples, Benjamin C. Pierce, 07/31/2019