Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

extensional trie map for positive #10

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

extensional trie map for positive #10

wants to merge 2 commits into from

Conversation

palmskog
Copy link
Member

WIP based on coq/coq#17044.

@palmskog
Copy link
Member Author

Hi @andres-erbsen, would you be interested in collaborating on getting the extensional trie from coq/coq#17044 implemented for the MMap interface? In this PR, I adapted the code from your PR based on the PositiveMap we already have here.

Some questions I have been pondering:

  • how does one implement the binders function for the trie?
  • how does one expose the extensionality in the best way in the TrieMapAdditionalFacts module?

Any hints or help appreciated.

@andres-erbsen
Copy link

Thank you for getting started at the integration here and reminding me that this is on my todo list still. I think bindings could be implemented like values and extensionality could be exposed by defining Equal as Logic.eq.

@palmskog
Copy link
Member Author

OK, I will take a stab at bindings using the values approach. However, for the Equal thing, unfortunately Interface.v defines Equal as something more general that we can't change if we want to implement the module type.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants