The Coq mailing list

[Coq User <coquser AT googlemail.com>]

But SpecialObject is Coinductive.  I've changed Singleton to be Coinductive and the problem is still there.  I need singleton:SpecialObject as opposed to singleton:Object.

Require Import String.
Require Import List.

Section Example.

(*Encoding of the Standard Example MetaModel*)
(*Top*)
CoInductive Top:Set :=
| Build_Top (name:string)
with 
Object:Set :=
| Build_Object (features:list Feature)(super:Top)
with 
Feature:Set :=
| Build_Feature (superfeat:Top)(featOwningObject:Object)
.
(*SpecialObject*)
CoInductive SpecialObject:Set :=
| Build_SpecialObject (info:string)(superObj:Object)
with 
Singleton:Set :=
Build_Singleton (superSingleton:SpecialObject).

(*Singleton Functions*)
(*Top Functions*)
Definition superSingleton:Singleton -> SpecialObject:=               
     (fun d:Singleton =>
         match d with
         | (Build_Singleton sup) =>sup
         end).
Coercion superSingleton:Singleton >-> SpecialObject. (*Type Coercion*)

(*Top Functions*)
Definition name:Top -> string:=               
     (fun d:Top =>
         match d with
         | (Build_Top elName) => elName
         end).

(*Object Functions*)
Definition features:Object -> list Feature:=               
     (fun d:Object =>
         match d with
         | (Build_Object feats sup) => feats
         end).
Definition super:Object -> Top:=               
     (fun d:Object =>
         match d with
         | (Build_Object feats sup) => sup
         end).
Coercion super : Object >-> Top. (*Type Coercion*)

(*Feature Functions*)
Definition featOwningObject:Feature -> Object:=               
     (fun d:Feature =>
         match d with
         | (Build_Feature sup p) => p
         end).
Definition superfeat:Feature -> Top:=               
     (fun d:Feature =>
         match d with
         | (Build_Feature sup p) => sup
         end).
Coercion superfeat : Feature >-> Top. (*Type Coercion*)

(*SpecialObject Functions.*)
Definition info:SpecialObject -> string:=               
     (fun d:SpecialObject =>
         match d with
         | (Build_SpecialObject inf sup) => inf
         end).
Definition superObj:SpecialObject -> Object:=               
     (fun d:SpecialObject =>
         match d with
         | (Build_SpecialObject inf sup) => sup
         end).
Coercion superObj : SpecialObject >-> Object.




(*Instantiaing a SpecialObject is where the error occurs.*) 

(*SpecialObject Metamodel Instance*)
CoFixpoint singleton:SpecialObject := 
    Build_Singleton (*Several Levels of Inheritance*)
    (   (*Supertype of Singleton*)
        Build_SpecialObject "someString"
        (
           Build_Object (*Supertype of SpecialObject*)
           (featureOne::featureTwo::nil) (*List of related Example Feature*)
           (
               Build_Top (*Supertype of Object*)
               "singleton" (*Name.*)
           )
       ) 
    )
with
featureOne:Feature :=
    (
        Build_Feature
        (
            (Build_Top (*Supertype of Feature*)
            "featureOne" (*Name.*) 
            )
         
         ) singleton
     ) (*Object that owns the Feature *)
with
featureTwo:Feature := 
    (
        Build_Feature(
          Build_Top (*Supertype of Feature*)
          "featureTwo" (*Name.*)
        )
     ) 
     singleton (*Object that owns the Feature*)
.
End Example.

On Tue, Aug 25, 2009 at 7:04 PM, Tom Harke <harke AT cs.pdx.edu> wrote:

When you use CoFixpoint the result type must be CoInductive.
So, I can get your example to check if I change
> CoFixpoint singleton:SpecialObject :=
to
> CoFixpoint singleton:Object :=
though I don't know if this is what you want.