The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

I suppose you want the inductive type that defines the logic language of Coq. It is in the source code, in Ocaml, in the directory kernel/term.mli

On Tue, Jun 4, 2013 at 5:51 AM, fengsheng <fsheng1990 AT 163.com> wrote:

Dear All:
     I'm working on a project which trys to transform the UML model to Coq by
using Kermeta.I am confused by the coq metamodel found in the Internet:
package COQ {
        abstract class Type {
                attribute name : String;
        }

        class InductiveType  extends Type {
                attribute isAbstract : Boolean;
                reference hasComponents [1-*]: Component;
                reference subTypes [0-*]: InductiveType;
                reference superTypes [0-*]: InductiveType;
        }

        class Component {
                attribute name : String;
                reference hasType [1-1]: Type;
        }

        class Option extends Type {
                reference hasType [1-1]: Type;
        }

        class List extends Type {
                reference hasType [1-1]: Type;
        }

        class BasicType extends Type {
        }

        class Enumeration extends Type {
                attribute values[1-*]: String;
        }

        datatype Boolean;
        datatype String;
        datatype Integer;
}
  I just want the basic type: Inductive, Enum, primitive. How does the
arrow(maybe in Inductive type) represent in the coq metamodel or counld you
give me a entire coq metamodel?