coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Transparent/Opaque?

From: "Randy Pollack" <rap AT dcs.ed.ac.uk>
To: coq AT pauillac.inria.fr, coq-club AT pauillac.inria.fr
Subject: Transparent/Opaque?
Date: Tue, 4 May 1999 12:54:22 +0100 (BST)

What have I done wrong to see this this:

  Coq < Print eqs.
  eqs =
  [T:CSetoid; n:nat; l,k:(listn (T) n)]
   (i:(fin n))
    (#GENTERM (CONST #listn#nth.cci) i l)
       [=] (#GENTERM (CONST #listn#nth.cci) i k)
       : (T:CSetoid; n:nat)(listn (T) n)->(listn (T) n)->Prop

Is it about Transparent/Opaque?

Randy

Transparent/Opaque?, Randy Pollack
- Re: Transparent/Opaque?, Patrick Loiseleur