coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Jasper Hugunin <jasperh AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Why can't unit be a primitive record?
Date: Sat, 16 Sep 2017 07:39:00 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasperh AT cs.washington.edu; spf=None smtp.mailfrom=jasperh AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-vk0-f43.google.com
Ironport-phdr: 9a23:tqosVRZaM3wSgi6cD26DWWX/LSx+4OfEezUN459isYplN5qZpsq5bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76vnYuHUD0MhMwLeDoEKbTid623qa84c79eQJN0Ri0eqt/Nl2WsArMsMgQyd9gI70pxwHJinBTPftf3mNpI12PmBC668utqs0wux9Msu4sopYTGZ7xeL41GORV

Hello,

I became curious as to why the unit type can't be defined as a primitive record:

```

Set Primitive Projections.

Record one := oo { }.

one is defined as a non-primitive record

The record one could not be defined as a primitive record

[non-primitive-record,record]

Fail Definition test_eta : (fun _ => Set) = (fun 'oo => Set) := eq_refl.

```

As above, it might be nice to have a judgemental eta rule for the unit type.

Regards,

- Jasper Hugunin

[Coq-Club] Why can't unit be a primitive record?, Jasper Hugunin, 09/16/2017
- Re: [Coq-Club] Why can't unit be a primitive record?, Pierre-Marie Pédrot, 09/16/2017
  - Re: [Coq-Club] Why can't unit be a primitive record?, Jasper Hugunin, 09/17/2017
    - Re: [Coq-Club] Why can't unit be a primitive record?, Guillaume Melquiond, 09/17/2017