On 2019-04-30 13:34, Emilio Jesús Gallego Arias wrote: > Clément Pit-Claudel <clement....@gmail.com> writes: > >> That's indeed a problem. In F* we used a fancy trie structure that >> gets updated every time an identifier is added to the context, and >> rolled back when reverting a segment. Maybe that would work for Coq >> too? > > You told me about this but I forgot, what kind of matching capabilities > does the trie have? > > Note that Coq already a "quasi-trie", which allows for efficient > prefix-matching, but I deem that far from enough.
The completion data structures in F* allow for prefix matching across each '.' in the qualified name, so Aaa.Bbb.Ccc can be found using A.B.Cc or B.Ccc or C.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
