coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] MSetFullAVL location

From: Jim Apple <coq-club AT jbapple.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] MSetFullAVL location
Date: Sun, 12 Sep 2010 10:24:24 -0400

In the 8.3rc1 sources, MSetAVL.v refers the reader MSetFullAVL for
proofs of the balance conditions and for non-structually-recursive
functions for a few operations, but MSetFullAVL.v is not in
theories/MSets.

Doe anyone know where I might find MSetFullAVL.v? I did find
FMapFullAVL.v in theories/FSets.

Jim

[Coq-Club] MSetFullAVL location, Jim Apple
- Re: [Coq-Club] MSetFullAVL location, Thomas Braibant
- Re: [Coq-Club] MSetFullAVL location, Pierre Letouzey