小编mdg*_*rge的帖子

我正在处理包含大量unicode字符(≼,⊓,⊔,...)的文本文件.Vim显示它们很好,但是当我打印时它们被一般字符替换.Gedit打印它们没有问题,但是为了打印而启动另一个编辑器有点痛苦.

有没有办法让vim(在Linux/Gnome上)正确打印？我尝试使用vim-gnome,希望它使用与gedit相同的基础设施,但事实并非如此.

我发现自己要一遍又一遍地重复一个模式，我想对它进行抽象。我相当有信心coq具有足够的表现力来捕捉模式，但是我在弄清楚如何做到这一点上有些麻烦。我正在定义一种编程语言，它具有表示语法术语的相互递归的归纳数据类型：

Inductive Expr : Set :=
  | eLambda  (x:TermVar) (e:Expr)
  | eVar     (x:TermVar)
  | eAscribe (e:Expr)  (t:IFType)
  | ePlus    (e1:Expr) (e2:Expr)

  | ... many other forms ...

with DType : Set :=
  | tArrow (x:TermVar) (t:DType) (c:Constraint) (t':DType)
  | tInt

  | ... many other forms ...

with Constraint : Set :=
  | cEq (e1:Expr) (e2:Expr)
  | ...

现在，我需要在这些类型上定义许多功能。例如，我想要一个函数来查找所有自由变量，一个函数来执行替换，以及一个函数来拉出所有约束的集合。这些函数都具有以下形式：

Fixpoint doExpr (e:Expr) := match e with
  (* one or two Interesting cases *)
  | ...

  (* lots and lots of boring …