Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] FSet Extensionality Not defined

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] FSet Extensionality Not defined


chronological Thread 
  • From: Taral <taralx AT gmail.com>
  • To: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] FSet Extensionality Not defined
  • Date: Wed, 18 Mar 2009 11:43:58 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=n4/Pq8SZfPBDfmOM3l/KJbLsSPBViGsQLylWbKSXwz1OmrjjiwK949NOOYngNswIWl KJHwis1VRGeWgAx9UMQ6UNtgcOFDtbN4GR34ArdRksM4lgJrVCUQx9GG80wl8dBJ6JjP Jw90K+LYWvpDa0BEjue0/TqJHpZZ8zXqlwPnM=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Wed, Mar 18, 2009 at 11:20 AM, M. Scott Doerrie 
<mdoerri AT cs.jhu.edu>
 wrote:
> I would really like to have an axiom-free method of constructing Ensembles
> from FSets.  However, I can't find any definition for
> Extensionality_Ensembles in FSetToFiniteSet in any version of the Coq
> standard library.  I believe this axiom would be derivable if creating FSets
> from UsualOrderedTypes, yet I can not locate it.  Did I miss something?  Is
> this not possible?

As far as I can tell, extensional equality of functions is not provable in 
Coq.

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown



Archive powered by MhonArc 2.6.16.

Top of Page