coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club AT inria.fr
Subject: [Coq-Club] functor application
Date: Thu, 27 Oct 2016 13:43:26 -0300 (UYT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta03.in.vera.com.uy 0562D227622
Ironport-phdr: 9a23:r+sQkxQJinzmhT7l0UQupQNbwdpsv+yvbD5Q0YIujvd0So/mwa64ZxGN2/xhgRfzUJnB7Loc0qyN4vqmBjVLsMfJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/mjabtotaCMk1hv3mUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6372cGU24Xm1JwDhLM8A39FsPpqTP3rONhxC6yI8DsRPY/XjHk8rY9G0ygszsOKzNsqDKfscd3lq8O+B8=

I don´t understand how is applied the functor defined

in NOrder inside module PeanoNat.

Regards

Patricia

[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