coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting

From: Alex Meyer <alex153 AT outlook.lv>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting
Date: Sun, 26 Aug 2018 15:47:51 +0000
Accept-language: lv-LV, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=alex153 AT outlook.lv; spf=Pass smtp.mailfrom=alex153 AT outlook.lv; spf=Pass smtp.helo=postmaster AT EUR03-AM5-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:fZ9IpxcEWawKKzAgbCKPxjl6lGMj4u6mDksu8pMizoh2WeGdxcuyYx7h7PlgxGXEQZ/co6odzbaO7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahY75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyhqR5wzJLbb4yOLvVyYr/RcMkGSWZdQMpcUTFKDIOmb4sICuoMJfpVr43jqFoBsBCwAhejBePxxT9Sm3T72rc10+A/HgDJwQAtH9wDvW/TrNXoKKcSVee1zK7LzTnZa/NWxy7w5Y7VeR4iufGBRb19fdbLxUQrCQ/JlFedpZD/Mz+L1ekBq2ab4PRjWO6zjmMqrgN8riWzysouj4TEhpgax1/B+Cpk3ok6OMG0RUt6bNOqDJddtyeXPJZsTMw4WWFnoiM6x6UGuZGleCgKz4wqyRHRZPKbb4SF7AvvWfqWLzp4nX5lf6mwiAio/Uin1+38StK70FFXripDj9bArGgN1wbU6sibVPRy4luh2TeI1wDV8O1EJl00lbbfK54mxb4wlYAfvljEHi/zgEn2jamWeVs4+uWw5Onrfq/qq5uCO4NuiAzyLr4iltK8DOggNwgBRWmb+eCy1L35+k35Ra1HgecykqbHv5HWOMQWq6CiDg9Sz4Yj9xK/DzCh0NQbh3UHKExFdAqdj4f1I1HOPOz4DfCnjluwlzdr3unKMaHlApXQNXfOi6zhfLZ4605E0gU/19Ff55ROCrEAOv3/QEHxtMaLRiM+Zka/xP+iA9Fg3KsfX3iOC+mXKuma5VSP/6ckJ/SGTI4Tojf0bfY/sa3Al3g8zHYZcLnh+JYGZWrwSv1iLlXAPCHEhcodFWANvUw6Urq52xW5TTdPaiPqDOoH7TYhBdf+VNaRdsWWmLWEmRyDMNhTb2FCBEqLFC6yJYKZR/MLbyHUJtEzy2VYB4jkcJco0FSVjCG/06Bud7CG/TAEsZXk155x+b+LzExgxXlPF82Yllq1YSR0k2cPG2Bk8Z1F+Rc443LelK9yjrpfCMBZ4O5PXkEiL5nAwudmCtf0HAXcYtOOT1XgSdKjU2g8

No, I am not aware of Coq notation system yet. Please, can someone give the relevant link to documentation/tutorial for arriving at ASTs from Coq code?

Alex

[Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting, Alex Meyer, 08/24/2018
- RE: [Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting, Jason -Zhong Sheng- Hu, 08/24/2018
  - [Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting, Alex Meyer, 08/26/2018