coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Record sort
Date: Fri, 27 Jan 2017 16:19:38 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f43.google.com
Ironport-phdr: 9a23:fJgPkx9BSQsiM/9uRHKM819IXTAuvvDOBiVQ1KB52+0cTK2v8tzYMVDF4r011RmSDNmdtqIP0baempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwpFiCC9bL5xIxm6swrcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh8G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYIQVAOUcPOZYqpT2qFgUohu6BAmsGvngwSJPi3/o3Kw1yeAhEQDY3AM6BN8BrHHUrMjvOKgMTO+10bDFwDPeZP1VwTfw8IrFfx87rf2RQ759cdDdxEoxGw/fgVidp4roNC6P2OsXqWiU9e9gWPqvi2E5rwFxpSCixsI2hYnIgoIZ017F9SBlzIosK921R0B2bcSrEJtXsCGaOI92Td04T250vyY6z6UKuZ+9fCcU1JQq3xzSZvOdf4SV/B7uVPydLDRmiH5/d7+yiQ6+8U26xe39Usm03kxKri1AktTUqHACzQHc6smCSvdn/0auwzKP1wHN6u5eOk01m7TUK4U9wrIqipUTtFnDEjXol0rrka+abl8k9fSw6+T7frXmoYeROJNzigHnK6ghhsi/AfkjPQUVRGia+eG81KX58kHjQbVKiOc2kqjDv5zAK8QbvP3xPwgA2YE6rh27Ej2O0dICnHBBIkgWVgiAit3XMl3PJbjKBPO+nV3kxCl5zvTHILTJCZDQaHXPjeGyLv5G90dAxV9rnphk7JVOB+RZLQ==

I do not understand why when I define a Record in sort "Type" it ends up in "Set"?

Welcome to Coq 8.6 (January 2017)

Coq < Record R (P: nat -> Prop) : Type := {f: nat -> nat}.

R is defined

f is defined

Coq < Check R.

: (nat -> Prop) -> Set

Vadim

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] Record sort, Vadim Zaliva, 01/28/2017
- Re: [Coq-Club] Record sort, Jan-Oliver Kaiser, 01/28/2017
- Re: [Coq-Club] Record sort, Hugo Herbelin, 01/28/2017
  - Re: [Coq-Club] Record sort, Guillaume Melquiond, 01/28/2017
    - Re: [Coq-Club] Record sort, Hugo Herbelin, 01/29/2017
      - Re: [Coq-Club] Record sort, Hugo Herbelin, 01/29/2017