coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] functor application

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] functor application
Date: Fri, 28 Oct 2016 09:48:00 +0200

On 10/27/2016 06:43 PM, Patricia Peratto wrote:

I don´t understand how is applied the functor defined
in NOrder inside module PeanoNat.

Regards
Patricia

It is a kind of chinese doll

PeanoNat includes NBasicProp which collects all the basic properties of a reasonable implementation (what is called Abstract) of natural numbers.

NBasicProp contains in particular NOrder.

--
Laurent

[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