Coq 8.6でFMapを使用する適切な方法は？

Question

Coqでツリーベースのマップ、特にCoq.FSets.FMapAVLを使用しようとしています。

私はこの4歳の質問が見つかりました：Finite map example

コメントで参照標準のlibのドキュメントを見て、私はこのノートを参照してください。

NB：このファイルは、以前との互換性のためだけにここにあるのFSetsとFMapのバージョン。今すぐStructures/Orders.vを使用してください。

これはどういう意味ですか？私がgoogle "Structures.v"または "Orders.v"を書くと、私はいつも他のドキュメンテーションページに関連して廃止予定の警告が表示されます。

Coq 8.6でFMapを使用するには、非推奨の非推奨の方法は何ですか？

Answer 1

OrderedTypeExモジュールは廃止されているため、Nat_as_OTは定義されていません。

OrdersEx（ちょうどPeanoNat.Natの同義語）にNat_as_OTがあります。これは私たちの目的に役立ちます。署名がOrderedType.OrderedType（現在FMapAVLによって使用される）とOrders.OrderedTypeは互換性がないため

残念ながら、次のコード

Require Import Coq.Structures.OrdersEx. 
Module M := FMapAVL.Make Nat_as_OT. 

は、動作しません。しかし、OrdersAltモジュールには、あるタイプのモジュールを別のモジュールから構築することを可能にするファンクタが含まれています。この場合、私たちはBackport_OTに興味があります。次のコードは、コードの残りの部分は、リンクされた質問からコピーすることができ、FMapAVL.Makeを使用する方法を示しています。FMapAVLはthis Coq-Club postにピエールLetouzeyで説明したと

From Coq Require Import 
FSets.FMapAVL Structures.OrdersEx Structures.OrdersAlt. 

Module backNat_as_OT := Backport_OT Nat_as_OT. 
Module M := FMapAVL.Make backNat_as_OT. 

状況：

間の遷移旧式のOrderedTypeと新しいものはが完了していません（例えばFMapsの作業がまだ残っています）。 と旧式のOrderedTypeを単に削除することはできません。