coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] FMap properties
- Date: Tue, 24 Feb 2009 01:21:24 +0000 (GMT)
- Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.co.uk; h=Message-ID:X-YMail-OSG:Received:X-Mailer:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type; b=33+IFppcA5U3Fi1JSaiKZp3uP/Pt0Oi0Zbj4tfLMtwoQ8w0hTefArqBVXXkiR2T7srixBsILyMKLmp3F+XqnlyHurBigeTLktpjHDvYuPnlxBPLO44GFOKj6+TitgbRWL11RSS7U2sXc2moOihVyt6w0zV5eFMgd2pzHFc9cFMA=;
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Am trying to prove a lemma on maps
Require Import FMapAVL.
Module FMap := FMapAVL.Make(Z_as_OT).
forall (tbl:FMap.t (list Z)),
(FMap.is_empty tbl = true) ->
forall (key:Z), (FMap.find key tbl = None).
but not sure where to start. I tried adding the property not_find_iff
by invoking
generalize FMap.not_find_iff.
but Coq (8.2) complains that it can't find this lemma, it can find
some of the others in the FMapAVL library though.
Ashish
- [Coq-Club] FMap properties, Ashish Darbari
- Re: [Coq-Club] FMap properties, Pierre Letouzey
Archive powered by MhonArc 2.6.16.