coqssreflect

string comparison in ssreflect


I'm trying to make an ssreflect OrdType out of a custom type which involves strings. I assume that there is some inbuilt order type for strings in ssreflect, but I can't find it anywhere. I see one in Coq's standard library, but I can't figure out if the definition transfers to the ssreflect library. I'd much rather use ssreflect than the Coq standard library. Could someone point me where to look please? Thanks.


Solution

  • unfortunately OrdType is not the order that has been integrated to mathcomp/ssreflect package in the end (Coq-Combi preceeds this integration), but it follows the same scheme. Which order do you want? Lexicogrphic? Prefix? Suffix?