问题描述
我正在尝试从涉及字符串的自定义类型中选择OrdType。我假设ssreflect中的字符串有一些内置的订单类型，但是我在任何地方都找不到。我在Coq的标准库中看到了一个，但是我不知道定义是否转移到了ssreflect库中。我宁愿使用ssreflect而不是Coq标准库。有人可以指出我在哪里看吗？ 谢谢。
解决方法
不幸的是，{'name': 'Jeremiah','course': 'Data'}
{'name': 'Domascus','course': 'Web'}
并不是最终集成到 mathcomp/ssreflect package 的顺序（Coq-Combi 在此集成之前），但它遵循相同的方案。
你要哪个订单？辞典？字首？后缀？
- 如果你想在 mathcomp/ssreflect 中使用字典序和标准化顺序，我建议你使用
OrdType和String之间的同构以及后者的词法排序来定义总序字符串（您需要为list ascii提供一个orderType规范结构）。 - 如果你想要一个前缀序，你可以证明
ascii函数是一个偏序。