coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor

From: Coq User <coquser AT googlemail.com>
To: harke AT cs.pdx.edu, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor
Date: Sun, 30 Aug 2009 15:50:46 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=k9XD1vhes2Pxyri0hyyMaqMquLVxypVtTlxS6ubmwmlLMbQu0aFyzEKR3OJcg2R2AR BUpdarrsLy1kkkQku3JdM5MvgwAA8jbw7KqLT2Sb8fmH2GNmloaTJKfYiOCQFR9F8lNh SVmYR7f8icIAaEMa/WzBkA9bmTS+lyqJ9iSXc=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Yes it seems to be.� I added the final line to Build the Singleton Type.

CoFixpoint singleton':Object :=
� Build_Object (featureOne::featureTwo::nil) (Build_Top "singleton")
with featureOne:Feature :=
� Build_Feature (Build_Top "featureOne") singleton'
with featureTwo:Feature :=
� Build_Feature (Build_Top "featureTwo") singleton'
.
Definition singleton:SpecialObject := Build_SpecialObject "someString" singleton'.
Definition s:Singleton := Build_Singleton (singleton).

[Coq-Club] Re: Recursive call on a non-recursive argument of constructor, Coq User
- Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor, Tom Harke
  - Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor, Coq User
    - Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor, Tom Harke
      - Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor, Coq User
        
        Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor, harke
        
        Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor, Coq User