coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is there a way to see the index of sort Type?

From: "Wan Hai" <wan.whyhigh AT gmail.com>
To: "Coq Club" <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] Is there a way to see the index of sort Type?
Date: Wed, 25 Jun 2008 09:40:38 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type; b=KVyAwE03xvlHYdM1oBkmDOgS+H74e88v7U0+QEMaWk9Z8l9zGrfrQfQVMsGe7x/jz5 0EhxRQHu1mZbJBm4ROzs8JZ5ZyAqxu0WeLXih9vdFA1eEHWWMRzJbBAmKUE+gyzD62s7 4HvlGb6z9GczMX+gJ6p4s+r5Br1yehKHYezdg=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear all,

When checking the type of an _expression_ using the Check command, you will possibly get a Type sort, such as:

Check (Type->Type).

you will get :

Type -> Type
: Type

Is there a way to let me see the exact index of Type. Such as, when I typed "Check (Type->Type)", it will replies me with:

Type(0) -> Type(0)
: Type(0)

Thanks!

--
Best regards,
Hai Wan

[Coq-Club] Is there a way to see the index of sort Type?, Wan Hai
- Re: [Coq-Club] Is there a way to see the index of sort Type?, vsiles