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.
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?
String
and list ascii
and the lexical ordering on the latter to define a total order on string (you need to provide a orderType
canonical structure for ascii
).Strings.prefix
function is a partial order.