Clément Pit-Claudel <clement....@gmail.com> writes: > 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.
Thanks Clément; I think that Coq's Nametab can do this kind of stuff already, I didn't look too closely tho. Current support is just an experiment and not well thought-out. I just added to SerAPI a complete command to see a bit more output: (Query ((pp ((pp_format PpStr)))) (Complete d)) (Answer 5 Ack) (Answer 5 (ObjList ((CoqString Decimal.Little.double) (CoqString Nat.double) (CoqString Nat.divmod) (CoqString Nat.div2) (CoqString Nat.div) (CoqString dependent_choice) (CoqString Decimal.decimal) (CoqString decide_right) (CoqString decide_left)))) (Answer 5 Completed) So yeah it ignores the module part. [The in-prefix maps of the nametab are not tries themselves tho, so it simulates them with a range-search over the map] I am not sure about tying completion to a concrete data structure, for example I'd like a completion system to be flexible for example w.r.t. non-prefix search, approximate matching, etc... I guess that for Coq we will try to allow to plug custom indexers to the namespace operations so they can use their indexing method of choice. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
