coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] records ?
- Date: Mon, 6 Sep 2021 23:19:57 +1000
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version; bh=Zt+DsA+fvm+cJL1rqlPeCkPcyZJXEwHWYSy6000w2tM=; b=cDqZBMiXmACvkDE4Bltk+JSBAOSR4TvZj6vusZoiKuolw4ln53scXvPcL/Q5QXGvTiOd67VF7qa/gc3y4NwR0gHN8+CmLD+sRt8VQLv/iP3t/rg03ZoXnh+C7kv+0+GvkkIY8HgpdQ6bVavD920jdtJBIgTE28/jLuvxk4c5aueNro2p/z+c9nTssbEVZO6eg1Q/UIAsQDJb766BYd5KYq21oxhG0APTy3exdxLN4G2K6Ap24oLvIVqrudTXdeXZez1as/Km5eKJ2Nfmk/ICeV5xCuRlpF0V7No1ZrR6TgvSY4wIkB8x0xKKvkuqpLrzwmio5Ch3wKL81PCHRFuwGw==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=NV4LI0I7x9y+RZJTc/IkJ0zM7lzp9OS3BXbtpGAxNMrGOfRdjKkv+oI2l1Ltd0hBHBuaRCw5lt+DTt1kTINZ54rzLuA4oIvloWyW1Lozth9QmcewpsL2gUxC9iO6s3bdmhE1FwmH3ZJCWKZEM22xR62lTyRU2Y0dgfHsfGLTdXWUQEAE+QgYBmSnqLlLIMys2vB19an4PlANY3C7e5U4SKtxC+kU261NsXkT5vCOM020rX6vbtRuFlAws1Z/2XF1WOzU1izzgc/2xmKvs+tJsC+l7hmQc1H/SwWnpQMIhUQv2YFeGVtxj87u/ClxdTJBJFmAGS2dYqaYWgWTyVLw6w==
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME3-obe.outbound.protection.outlook.com
- Ironport-hdrordr: A9a23:sXy5la+nVLgljhDKPAhuk+FSdb1zdoMgy1knxilNoENuH/BwxvrFoB1E73TJYVYqN03I6urwQ5VoJkmsj6KdgLNhRYtKOTOLhILGFvAE0WKP+UyEJ8S6zJ8l6U4CSdkANDSTNykfsS+S2mDRfbdQseVvsprY59s2p00dMT2CAJsB0+4WMHf5LqQ7fnghOXJvf6Dsm/av6gDQM0g/X4CePD0oTuLDr9rEmNbPZgMHPQcu7E2rgSmz4LD3PhCE1lNGOgk/jYsKwCzgqUjU96+ju/a0xlv10HLS1Y1fnJ/ExsFYDMKBp8AJInHHixquZq5mR7qe1QpF7d2H2RIPqp3hsh0gN8N85zf4eXy0mwLk303a3DMn+xbZuBalqEqmhfa8aCMxCsJHi44cWADe8VAcsNZ1178O936FtrJMZCmw3BjV1pztbVVHh0C0qX0tnao4lHpES7YTb7dXsMg24F5VKpEdByj3gbpXUdWGNPuspsq+TGnqKkww5gJUsZiRtzUIb1m7q3E5y4+oO2M8pgE/86Nwr/Zv4Evp9/oGOu95Dqr/Q+JVfYp1P7wrhJRGdZA8qPuMexzwqC33QRCvyHTcZek60iH22tXKCItc3pDeRHVP9up8pL3RFFlCtWQ1YSvVeLmz4KE=
- Ironport-phdr: A9a23:nek5wxdnkMHfYfhaO8TBXkCylGM+D97LVj580XLHo4xHfqnrxZn+JkuXvawr0AWRG9SCoK8bw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PPbwlSgDexfLx+IRW0oA7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5LppRhD1kicKLyM3/n/ZisJwj6xVrhyuqB5jzIDbb46YL+Z+c6DHcN8GWWZMUMRcWipcCY28dYsPCO8BMP5coYbjvVsBsx6+BAmxD+3h0DBJiGT23ao80+88FgzI2BIvH8gQv3TRrNT5LqkcXvq7zanTyjXDaehb1i376IjVaBwuv+yDXa9qfcXL1EkiDgXIhUifpoL5JT2azPgNs3SF4Op6U+Kik2wqpg9xrzSzyckglpfFi4YJx13F9yh3z5s4KN+kRUN/b9OpHphduiGHO4Z2X84vQGNltik6xLAGtpO1cysHxZYhyhXCaPKHa5CF7x3/WOqLPDt0mHBodKiiixqu8kWs0PDwWtS73VpSsyZJjMXAumoQ2xHQ8MSLV/9w80m71TqR2A3e6edJKl0um6XBMZ4u2Lswm4ITsUvdGi/2n137gbOYeUs55uSk9v3rbLLpqJKSLoN0jRrxPbo0lsy4HOQ4LhMBX2+G+eS6ybLv51X5QK9Njv0qjKbWrIzaJcUcpq6/GQNV1Zsj6wq7Dzeh19QYnmMLI05CeBKCl4TpOlfOL+7kDfqnjFmgjC1ny+3aMrDjGJnBM2TPnbT7cbpg9kJRxxI/zdVF6JJVDrEBLujzWkj0tNHAChE2LRa0zPjiCNR9zI8QV3iAA6GCMKPVt1+F/fggI++RZIMPpjnyNuUl6+T0gn8kgVMdZ7Wm3YMLaHCkGfRrO1mWYX31gtsYDWgKuhc+Q/fxhV2ZUT9TYm6yULgm6jE6DoKmF4bDSZq3jLyPxifoVqFRM2tBExWHFWriX4SCQfYFLiyIceF7lTlRd7W7RoownT2nqxT9zfIzDOfO9ygJ877qy8Ny4cXakwx0+DBpSc2AhTLeB1pol38FEmdllJt0plZwnw/rOUlQqsFjTYUWwt4SFwAwONjb0vBwDM30VkTZZNCVRV26Q9KgRzYsUtY2xNxIaEF4SYzKZvXr1iy3RbIZivqCGc5smkoz93H3OoBwx2uA3bRz1jEb
On 6/9/21 2:57 pm, mukesh tiwari wrote:
However, in your case, I believe, it will be type error because {| c := ccc ; i := iii |} is not of Type, Set, or Prop.
Indeed.
Thanks for all the replies. Unfortunately the code I'd obtained and was building on had all sorts of coercions defined, so where Coq printed out
{| c := ccc ; i := iii |} it represented nothing of the sort, but when I typed it into the computer (making serious efforts to try to figure out what was going on), it represented exactly the record it looks like.
Thanks for all your time replying.
Jeremy
- [Coq-Club] records ?, Jeremy Dawson, 09/06/2021
- Re: [Coq-Club] records ?, Agnishom Chattopadhyay, 09/06/2021
- Re: [Coq-Club] records ?, Jeremy Dawson, 09/06/2021
- Re: [Coq-Club] records ?, Agnishom Chattopadhyay, 09/06/2021
- Re: [Coq-Club] records ?, Jeremy Dawson, 09/06/2021
- Re: [Coq-Club] records ?, Agnishom Chattopadhyay, 09/06/2021
- Re: [Coq-Club] records ?, Madhukar, 09/06/2021
- Re: [Coq-Club] records ?, Agnishom Chattopadhyay, 09/06/2021
- Re: [Coq-Club] records ?, Jeremy Dawson, 09/06/2021
- Re: [Coq-Club] records ?, mukesh tiwari, 09/06/2021
- Re: [Coq-Club] records ?, Jeremy Dawson, 09/06/2021
- Re: [Coq-Club] records ?, Agnishom Chattopadhyay, 09/06/2021
Archive powered by MHonArc 2.6.19+.