Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] records ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] records ?


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.19+.

Top of Page