coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types
Date: Tue, 15 May 2018 17:08:23 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga17.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:rYqoGxyuwAsiYgzXCy+O+j09IxM/srCxBDY+r6Qd2+4eIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMx+jq1boQ6uqBNwzYPPfIGVLf5zcr/Bcd8GW2ZMWNtaWSxbAoO7aosCF+QNM/tfr4bjqFsOsQG+BQ60BO/31zRGgX720rE60+s7Dw7G2AIsFM8JvXTRrdX6KKcSXvqrw6nM1znDdPRW1iny6IjUaBAhpumMUKlxccrX1UkgCQfFgk+MpoziOjOYz+IAuHWV4epnUOKgkW8nqwdprziuwMcslpfGhoYPxl/Z6yp0xps+K96gSENjfNKpFIVcuzuaOoZ2WM8vQ39ktDwnxrAGpJK3ZDUGxZUpyhLFZfGKfZKE7gztWeuVOzt0mXFodKynixqv8EWtzvfwWte03VtFtCZJjMPAum4C2hHX7MWMV+Fz8V272TmV0gDe8uFELl4wlarcM5Mhx7EwmYAOvUnBBCP2mUP2jLOIeUUg4OSn9+PnYrD+qp+dMY97lB3+P7wzlsG7H+g0KAgDUmiB9em8yrHv51D1TbVXgvEul6nWqpHaJcAVpq6jBA9V154u6xO+Dzi60NQXh2cILFZfdBKciIjmJV7OIOziDfe4m1ShizZrx/baPrL/BpXBNGTMkLDkfbpl8U5T1BIzzcxD55JTErwOPPXzWlbouNPECh85Lhe7zv38CNR904MeQXiADrWYMKPUq1+I5/ggL/OCZI8P637BLK1v7Pn3yHQ9hFU1fK+z3JJRZmryVqBtJFzcan7xiP8AF30Lt0wwVrq5pkeFVGsZXHG/UL4m4Sl/QKenBofKS4TnyOiE3Sy7F5BSIHtBB1+QC3DwX4SCR/oILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8/d7uGymgjrZvmkeNNyajWnBA2+yZzCp3EgWCLU2xw2GgPQm1vhfwtkQlG0l6GlJNArblAD9UKvqFIVBs3MdjXyOkoU4mvCDKERc+ATROdevvjATw1SYtukdoBah8iXdSkkh3HmSGtBu1Nmg==

Dear Maximilian,

thanks for the hints, quite useful - at least for reducing my confusion when
looking at terms. I did experiment a bit with abstract, but when used
together with e.g. ltac: it doesn't have an effect.

@ Jason: my stuff is automation heavy and requires a lot of boilerplate code,
but I will setup a useful example tomorrow.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] "Opaquify operator" to simplify work with dependent types, Soegtrop, Michael, 05/15/2018
- RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types, Jason -Zhong Sheng- Hu, 05/15/2018
  - RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types, Soegtrop, Michael, 05/16/2018
    - Re: [Coq-Club] "Opaquify operator" to simplify work with dependent types, Fabian Kunze, 05/16/2018
      - RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types, Soegtrop, Michael, 05/16/2018
- Re: [Coq-Club] "Opaquify operator" to simplify work with dependent types, Maximilian Wuttke, 05/15/2018
  - RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types, Soegtrop, Michael, 05/15/2018