Emacs下Coq/Proof General中关键字和运算符的Unicode字形

文章/答案/技术大牛

发布

1回答

emacs、unicode、elisp、coq、proof-general

这个问题与Emacs中Proof General中的Coq模式配置有关。我正在尝试让Emacs自动将Coq中的关键字和符号替换为相应的Unicode字形。问题是，当我尝试将运算符=>、->、<->等定义为它们的Unicode符号⇒→

浏览 5提问于2012-04-21得票数 9

回答已采纳

1回答

Coq + Emacs？`‘Emacs`’看不到源文件中定义的内容。

emacs、coq

因此，我正在使用Coq使用Emacs作为IDE。proof-general和company-coq都已正确安装和加载。然后打开虚拟whatever_name.v文件并使用Fixpoint关键字定义递归函数。检查addnm。错误:在当前环境中找不到参考地址not。

浏览 2提问于2021-07-21得票数 1

回答已采纳

4回答

如何在emacs中禁用Verilog模式？

emacs、proof-general

我尝试在ProofGeneral中使用coq，但是内置的Verilog模式遮蔽了*.v文件类型识别。我能以某种方式禁用它，让ProofGeneral将它们重新映射到它的coq模式吗？

浏览 6提问于2012-03-09得票数 5

回答已采纳

2回答

为什么某些Unicode字符在Emacs中不可见？

emacs、unicode

我一直在使用支持做一些技巧，而且在大多数情况下，它工作得很好。但是，并不是所有Unicode字符都显示出来，即使是在字体中也是如此。例如：上面(假设它被正确地呈现)有正常的ASCII字符、几个Unicode箭头和一个Unicode INTERROBANG (一个非常有用的字形，需要更广泛的使用)。然而，无论如何，Interrobang不会出现在Emacs中<

浏览 1提问于2013-04-29得票数 10

4回答

在类型类解析发散后卡在“回缩缓冲区”

coq

在使用类型类时，Coq有时会出现分歧。在Proof General下发生这种情况时，Emacs也会挂起。我所知道的最好的恢复方法是中断emacs (C-g)并重新启动Coq (C-c C-x)。但是，这并不是简单地终止Coq进程，而是将我置于Emacs再次挂起的模式中，并显示“正在收回缓冲区...”。相当长的一段时间(有时太长以至于我放弃了，只是开始一个全新<e

浏览 0提问于2018-02-04得票数 3

2回答

Agda可以在批处理模式下编译得更快吗？

compilation、incremental-build、agda

当我编译一个使用标准库的Agda程序时，编译器花了很长时间打印出如下代码行：有没有办法避免每次编译都要做这些额外的工作？

浏览 1提问于2012-03-15得票数 4

2回答

Emacs:用于在OSX中显示unicode字符的字体设置

emacs、fonts、osx-lion

我试图显示特殊的unicode字符，特别是emacs中的数学运算符。font e name: MATHEMATICAL BOLD SCRIPT SMALL E general-category上面的文本在我的浏览器和TextEdit中显示得很好，但是，当在emacs中查看时

浏览 0提问于2012-06-06得票数 8

回答已采纳

4回答

coqide -无法从同一文件夹加载模块

coq

我无法加载在CoqIde的同一文件夹中的模块。Error: Cannot find library Poly in loadpathRequire那么，你们是如何将程序从SF加载到coqide中的呢？

浏览 0提问于2013-04-25得票数 22

回答已采纳

1回答

存在主义的目标填写得太快了

record、coq、typeclass、coq-tactic

我有一个包含数据和公理的Class。我希望在验证模式下构建另一个实例，基于(1)现有实例和(2)其他输入。在创建记录的新实例之前，我希望destruct这第二个输入。作为示例工作的最小Class从中的最小值缩小Require Import Coq.Init.Datatypes.Require Import Coq.Classes.M

浏览 2提问于2018-07-13得票数 1

回答已采纳

3回答

Coq:用子目录管理项目中的LoadPath

coq

但是，我也希望使用/Coqtop来处理文件，在这种情况下，工作目录默认是文件所在的目录。我试过的每一种方法，都会出问题。例如，如果我通过调用Aux.v来编译 coqc -R "."然后，这在Coqtop中工作，但是在coqc -R &

浏览 3提问于2015-08-05得票数 8

回答已采纳

1回答

如何定义自动不可折叠的定义

coq

但是，这个定义似乎是抽象的，因为如果不首先展开，我就不能在g实例上使用关于g的定理： unfold g. rewrite f_unit.

浏览 0提问于2017-12-01得票数 4

回答已采纳

2回答

证明唯一长度为零的向量为零

coq、dependent-type

case a似乎是最接近的，但它得到了一个错误：fun (n : nat) (a0 : bits听起来它不能确定任意长度的位向量是否等于零长度的位向量，因为它们在类型级别上是不同的。对吗？

浏览 14提问于2017-12-23得票数 5

回答已采纳

2回答

在匹配中展开类型函数(如析构)

coq、dependent-type

根本的问题是Coq不会使用match来注意到这些类型在依赖类型中是等价的；我可以强制它在验证模式下，但是我想知道没有它是否有可能这样做。 Require Import Coq.Unicode.Utf8. generali

浏览 7提问于2021-03-30得票数 1

回答已采纳

1回答

为什么我的类型排序记录显示为Set sort？

coq

我创建了一个显示相同行为的最小测试示例： Record little_test : Type := bit1 : nat; }.

浏览 15提问于2019-04-25得票数 1

回答已采纳

1回答

是否仅使用iTextsharp get number提取阿拉伯文本？

text、itext、extract、arabic-support

我试图从PDF文件中提取阿拉伯文本，但它只提取数字和结果如下：我的代码： public static string GetTextFromAllPagesPdfTextExtractor.GetTextFromPage(reader, 1, new Locati

浏览 1提问于2018-04-24得票数 0

1回答

在哪里可以获得所有不同于简单字符的unicode字符的完整列表。例如:字符0x0363 (之前没有另一个字符将不会打印)，字符0x0084 (打印时会发生奇怪的事情)。我只需要这样一个不寻常的字符的原始列表，用一些无害的东西替换它们，以避免不想要的输出效果。常规字符(不在此列表中的字符)在打印时应只使用一个字符位置(=光标向右移动+1 )，不应依赖于前一个或下一个字符，并且不应以任何方式影响打印样式。我有一些

浏览 45提问于2021-11-03得票数 0

回答已采纳

2回答

Java PDFBox -读取和修改具有特殊字符的pdf (diacritics)

java、pdf、utf-8、diacritics、pdfbox

是类似于0002或0004的代码。截图：编辑2：在proces

浏览 27提问于2013-04-12得票数 8

回答已采纳

3回答

C类语言的Emacs模式

emacs、colors、development-environment、indentation、auto-indent

我正试图为一种新的类似c语言的模板编写一种新的emacs模式，这是我在一些学术研究中必须使用的。我希望代码像c模式那样被着色和缩进，但有以下例外：代码行不以分号结尾。是否可以创建派生模式(从c模式)并将其设置为忽略“%”和“；”的</

浏览 2提问于2012-02-24得票数 6

回答已采纳

3回答

在iOS5中以不同方式绘制的Unicode字符

objective-c、unicode、fonts、ios5

将but按钮的标题设置为u25C0会导致它在iOS5中具有蓝色背景，但在iOS4.3中则不是。这是通过将标题设置为前面所述的unicode字符来实现的。

浏览 2提问于2011-12-01得票数 10

回答已采纳

5回答

用于操作“=”的非法排序组合(utf8mb4_unicode_ci，显式)和(utf8_general_ci，强制)

mysql、ruby-on-rails、utf-8、collation

这个问题(也是在以下背景下提出的)：并得到以下错误：(utf8mb4_unicode_ci,EXPLICIT) and (utf8_general_ci,COERCIBLE我试着在Sequel中运行这个查询，它起作用了(有和</e

浏览 3提问于2015-09-10得票数 25

点击加载更多