标准ML是否支持Unicode？
我相信它没有,但找不到任何SML说明这样的权威文档.
是或否是所有需要,但你必须知道一个事实.没有猜测或我相信答案.权威链接会更好.
我正在寻找一个工具(首选GUI但CLI可以工作),它允许我输入数学表达式,然后执行它们的操作,但限制我只有数学上有效的操作.此外,该工具必须能够保存会话,然后证明给定的已保存操作集是有效的.
注意:我不是在寻找一个生成校样的系统,只是检查我手动指定的步骤是否有效.
我已经使用ACL2进行类似的操作,并且它在某些情况下表现很好但是很难用于其他所有情况.
这个小项目是我的动力.它是一种D模板类型,允许求解方程.鉴于这个等式:
(A * B) = C + D / F;
可以将任何一个符号设置为未知,并评估该表达式将导致对该变量的赋值.它的工作原理是将表达式树构建到类型中,然后使用重写规则将其转换为可以针对未知类型进行事件处理的事物.
我需要的是一些验证重写规则的方法.可以通过测试给定某种关系为真的断言来验证它们,另一种也是.
此问题与在Emacs中的Proof General中配置Coq模式有关.
我正在尝试让Emacs使用相应的Unicode字形自动替换Coq中的关键字和符号.我设法定义fun为希腊小写lambdaλ,forall作为通用量词符号∀等.我没有问题定义单词的符号.
问题是,当我尝试定义操作符=>,->,<->等他们的Unicode符号⇒→↔,他们不是在勒柯克相应的Unicode字形所取代.但是,*scratch*当我测试它们时,它们会在缓冲区中被替换.我使用相同的机制将Unicode glyps与Coq表示法匹配:
(defun define-glyph (string char-info)
(font-lock-add-keywords
nil
`((,(format "\\<%s\\>" string)
(0 (progn
(compose-region
(match-beginning 0) (match-end 0)
,(apply #'make-char char-info))
nil))))
))
我怀疑问题是Coq模式将某些标点符号标记为特殊标记,因此Emacs忽略了我的代码以用Unicode字形替换它们,但我不确定.有人可以帮我解释一下吗？
我正在尝试将coq与ProofGeneral一起使用，但是内置的Verilog模式遮盖了*.v文件类型识别。我可以以某种方式禁用它，让ProofGeneral将其重新映射到其CoQ模式吗？
我发现这polyml是可以在Ubuntu上轻松安装的ML的实现(在存储库中命名为polyml并且可以执行poly).我正在按照安德鲁·卡明的" A Gentle Introduction to ML".经过几分钟的polyml解释器实验后,我发现它不支持readline (按向上箭头键会产生^ [[A]).
对于口译员来说,这似乎不正常.这应该只在没有安装readline的情况下发生,但我的Python解释器不会这样做.
我正在尝试实现一个测试函数来比较并显示错误消息,如果它们不相等:
exception AssertionErrorException of string
fun assert(testName, actual, expect) : bool =
if actual = expect
then true
else raise (AssertionErrorException (testName ^ " failed. actual: " ^ actual
^ ", expect: " ^ expect ));
不幸的是,如果我用非字符串参数调用它,它就不起作用:
assert("test1", SOME [], NONE);
它无法编译,错误信息是:
Error: operator and operand don't agree [tycon mismatch]
operator domain: string * string * string
operand: string * 'Z list option * 'Y option
in expression:
assert ("test1",SOME nil,NONE)
怎么解决？
Isabelle/jEdit中的颜色代码是什么意思？我在Isabelle/jEdit手册中找不到他们的描述.它写的唯一的东西是
证明反馈通过颜色,框,波浪下划线,超链接,弹出窗口,图标,可点击输出工作 - 所有这些都基于Isabelle在后台制作的语义标记.
颜色用作校样脚本背景和滚动条旁边的垂直条.
你能指点一些文件或在这里解释一下吗？