coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq Club <coq-club AT inria.fr>
Cc: "Prof. Vladimir Voevodsky" <vladimir AT ias.edu>, Matthieu Sozeau <matthieu.sozeau AT inria.fr>
Subject: [Coq-Club] a question
Date: Sun, 30 Aug 2015 18:01:05 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vladimir AT ias.edu; spf=None smtp.mailfrom=vladimir AT ias.edu; spf=None smtp.helo=postmaster AT vpps2.ias.edu
Ironport-phdr: 9a23:raXMLBf8RJew0azDpfT1Os56lGMj4u6mDksu8pMizoh2WeGdxc68YR7h7PlgxGXEQZ/co6odzbGG6Oa/ACQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTskb/rs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faPPyRLw1XDW4p5lsRQHvhDwEJnZt7mXehs11jbhzoRu64RFz3tiHM8muKPNic/aFLpshTm1bU5MUDnQZDw==

Hello,

are the coercions, in Coq, always fully inserted before any computation?

Vladimir.

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail