coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: sunil <sarswat AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Connecting strings in Coq and extraction target?
- Date: Fri, 5 Oct 2018 23:19:22 +0530
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sarswat AT gmail.com; spf=Pass smtp.mailfrom=sarswat AT gmail.com; spf=None smtp.helo=postmaster AT mail-it1-f179.google.com
- Ironport-phdr: 9a23:Fr1Rkx2pOJAQGjjdsmDT+DRfVm0co7zxezQtwd8ZsewQKfad9pjvdHbS+e9qxAeQG9mDtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo68dJYPD+wAPeZcsoLwoEAOogGkBQm3CuLg0CNIi2T53a0/yeshEAXG0BY8ENIJtXTZtdP4P7oRX+Ct1KTE0ynPYvdM1Tr+6IXEaA0trPCNUL5qbMbcy00iGgXYhVuKs4PlJSma1uEVvmib8eVgUeWvhnYiqw5rozivwt4giojVho4I01zE+zh1zYQxKNGiR057ZtmkEJRUty6ELYd5XsQiQ2RwtCY7zL0Jp4K7cTAUxJg7wxPTcf+KfoiS7h7+VeucIC10iG9ndb+7nxqy9FKvyuz4Vsm6ylZKqS9Fn8HXtn8XzRzT8caGReFh/kq61jaP0hrc6uBAIUwuiaXbLJshzqYqlpUPqUTDAjP2mELugaCKcUUk4/Gk5PjjYrX7vZCRLJR0iwH7MqQ2gMOzG+U4Mg4UX2ia4+uwzrPj/VeqCIlN2/Yxi+zStI3QDcUdvK+wRQFPgag57BPqFCqg0dBQyWIONklacQ6vgI3gOlWIK/f9W6Tsy2+wmStmkqiVdobqBY/AeyCaweXROI1l4ksZ8zIdiNVW5pZaELYEeauhVUr4tdieBRg8YVXtn7TXTe5l34ZbYlqhR7eDOfqL41CN7+MrZeKLYd1N4WuvG70e//fryEQBtxodcK2uh8VFbXm5GrFnPxzcbyOz05EOFmAFugd4R+vv2gWP
On Fri 5 Oct, 2018, 9:26 PM Jason -Zhong Sheng- Hu, <fdhzs2010 AT hotmail.com> wrote:
Hi all,
I am wondering if there is already a good practice on turning strings in Coq into, say, strings in Haskell?
And, this populations increase ,
The goal is to push informal part as late as possible, so I am thinking implementing the to-string functions in Coq as well.
Coq:= a machine, better you understand, better you perform, focus on understand.
This is especially important when the objects are dependent.
Machine can solve this problem.
However, these strings need to go to console eventually, so I guess it has to become string in Haskell some point.
Apropose is a Linux command. Other is grep.
My problem is, if this transition is not well-guarded, it sort of defeats the purpose of pushing informal parts late already.
Human is part of only one fourth of the mother Earth.
So how do people normally do this?
Easy, try to understand अहिंसा.
Secondly, is there any framework that can turn a context free grammar into a certified parser in Coq?
.
Thanks,Jason
- [Coq-Club] Connecting strings in Coq and extraction target?, Jason -Zhong Sheng- Hu, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, Ifaz Kabir, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, Xuanrui Qi, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, Jason -Zhong Sheng- Hu, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, Xuanrui Qi, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, sunil, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, Ifaz Kabir, 10/05/2018
Archive powered by MHonArc 2.6.18.