coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Is there something like especialize?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Is there something like especialize?
Date: Mon, 30 Apr 2018 12:34:31 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.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 mga09.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:mnlrTxVUkjKTzkj4J1e8vTTjxHnV8LGtZVwlr6E/grcLSJyIuqrYbBGFt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRxxwYHUYZ2aO/VxcK7GYdMVXm5MUtpNWyBdAI6xaZYEAeobPeZfqonwv1UCowa5BQayC+Pv1iVIhnju3aEizu8vFgDG0xAgH90UrnvUqNv5P7oVXOCwzanH0TXDYOlI1jf58oTIaRchru+DXbJsa8rRzlEvGhjEjlWWtYzqITeV2v4RvGic6uptTOSigHMppQF2pzig3MYsio/Ri4IUzFDE6Tt2wIIvKdKlVkF2Z8OvHphItyyCKod7TMwvT3t1tCs0xbAKo4O3cSYLxZg92RLSZOSLf5WJ7x/tTuqcLzl1iGh7dL+xgxu+61Wsx+7gWsWszVpHry5InsPSun0N2BHf8NaLRuFj8kqu3TuC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBir2mErsg6OKckgo4Omo6+L7Yrr4op+QLZN7igb7Mqg2m8y/B/o3MhQWUmSG9+mx26fv8VD3TbhFlPE6j6fUvZHAKcgFqaO1GwpV3Zwi6xa7ATemytMYnXwfIVJAeRKIk4jpNEvQL/D8F/u/mFOsnylkx/DaJL3hBY3NI2PCkLfnYbZy9UpcxBAvwtBY4pJYEqsBL+7rWk/tqNzYCQc0PBCzw+b+EdlyyoceWX+UDaKCK6PTsVqI5vo1LOWWZY8Vviz9K/k/6PL0g385gwxVQa78l5AQcTWzGulsC0Sfe3vlxNkbWy9etQ0nCefulVeqUDhJZn/0UbhqtR8hD4fzR7zES4+xmruZmG+eH5ZWb21CQBjYFHbjd4yJX7EXby+dPtVmihQFU6SsT8kq0hT451yy8KZuMueBon5QjpnkztUgv7SCxyF3ziR9CoGm60/ISmh1mm0SQDpvhfJ+p1BwzhGI1q0q2qUER+wW3OtAV0IBDbCZ1/ZzUomgWwTdc9PPQ1GjEI3/XGMBC+kpytpLWH5TXtWviheagHivDLZNxvqKAoA59uTX2H2jf8s=

Dear Pierre,

> I think [eapply t] means "I want to instantiate all hypothesis of t, make
> evars
> with unsolved parameters". But with specialize there is one more level of
> freedom as I said above: leave some hypothesis uninstantiated. We should
> have
> a way to tell that to especialize imho.

You are right. I am using specialize mostly in automation where I do one
precondition after another. If you care only about the first precondition,
there is not much difference between specialize and apply, but I completely
agree that for specialize there is a more general case.

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] Is there something like especialize?, Soegtrop, Michael, 04/30/2018
- Re: [Coq-Club] Is there something like especialize?, Pierre Courtieu, 04/30/2018
  - RE: [Coq-Club] Is there something like especialize?, Soegtrop, Michael, 04/30/2018
    - Re: [Coq-Club] Is there something like especialize?, Pierre Courtieu, 04/30/2018
      - RE: [Coq-Club] Is there something like especialize?, Soegtrop, Michael, 04/30/2018