coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Module Types

From: Cedric Auger <Cedric.Auger AT lri.fr>
Cc: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] Module Types
Date: Thu, 18 Jun 2009 18:29:51 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi all,

Is there any special reason to forbide the proof-editing mode in Module Types and allow Definitions?

Since the proof editing mode is just a way to build Definitions, I don't see the reason to allow directly writing lambda terms but not to use the tools to build them.

--
C�dric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay

[Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
- Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
- Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Matthew Brecknell
  - Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Matthew Brecknell
    - RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
      - Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
        
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
        
        Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
        
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
        Message not available
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
    - [Coq-Club] Module Types, Cedric Auger
      - Re: [Coq-Club] Module Types, Elie Soubiran
        
        Re: [Coq-Club] Module Types, Cedric Auger