Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] a problem with canonical structures

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a problem with canonical structures


chronological Thread 
  • From: Cyril Cohen <cohen AT crans.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] a problem with canonical structures
  • Date: Sun, 17 Apr 2011 21:20:05 +0200

Hi,

On 17/04/2011 21:08, Vladimir Voevodsky wrote:
> Consider the following code:
> [...]
> Coq complains that  "Error: X is not a structure object.". What is then a 
> "structure object"?

I suppose it means that the fields of the structure should be
instantiated in order to be inserted into the Canonical Structure table.

Here is an example of fix :

Variable T : Type.
Variable P : T ->  Type.

Structure TP: Type := {pr1:>T ; pr2:P pr1}.

Variable p1 : T.
Variable p2 : P p1.

Canonical Structure X := {| pr1 := p1; pr2 := p2 |}.


Best Regards,
-- 
Cyril Cohen
Sorry for the duplicated reply



Archive powered by MhonArc 2.6.16.

Top of Page