coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] functor application

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] functor application
Date: Fri, 28 Oct 2016 08:17:06 +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 mga06.intel.com
Ironport-phdr: 9a23:2elOsxQa+IOTquU5Dp+dA5/q/Npsv+yvbD5Q0YIujvd0So/mwa64YhON2/xhgRfzUJnB7Loc0qyN4vqmBjZLuM3a+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrr0pMeYOl4TzBOGIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvCwdKMhCLdcET4OMmYv5cStuwOJBV+E4WJZWWELmDJJBRLE5Vf0RMGinDH9s7834y6XMtHsSqhwERGj5KdiRRuiwHMCNjU5+WzTzNd3ga1HuhW5jx1534PQJoqSMawtLevmYdoGSD8ZDY5qXCtbD9bkYg==

Dear Laurent,

> It is a kind of chinese doll

In Germany we call it a Russian doll. Indeed the module structure of many
libraries has similarity with this picture:

https://russianlegacy.com/semenov-20-piece-russian-doll-p-2898.html

except that at each level you have several ancestors and several children ;-)

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] functor application, Patricia Peratto, 10/27/2016
- Re: [Coq-Club] functor application, Laurent Thery, 10/28/2016
  - RE: [Coq-Club] functor application, Soegtrop, Michael, 10/28/2016
    - Re: [Coq-Club] functor application, Laurent Thery, 10/28/2016
      - Re: [Coq-Club] functor application, Robert Merkin, 10/29/2016
- RE: [Coq-Club] functor application, Soegtrop, Michael, 10/28/2016