小编Maë*_*lan的帖子

我已经MongoDB在我的Mac上安装了几天,并且不确定我是如何安装的,但是现在如何检查MongoDB我的系统是否正常运行？

OCaml 对于多态类型注释有几种不同的语法：

let f :         \'a -> \'a = \xe2\x80\xa6 (* Isn\xe2\x80\x99t this one already polymorphic? (answer: NO) *)\nlet f : \'a.     \'a -> \'a = \xe2\x80\xa6\nlet f : type a.  a ->  a = \xe2\x80\xa6\n

当使用奇特的代数数据类型（通常是 GADT）时，我们经常会看到它们，它们似乎是必要的。

这些语法有什么区别？何时以及为何必须使用每一项？

我目前正在学习 OCaml，尤其是函子。map.mli我从标准库中查看，在第 70 行左右，有：

type key
(** The type of the map keys. *)

type !+'a t
(** The type of maps from type [key] to type ['a]. *)

val empty: 'a t
(** The empty map. *)

我知道这key是映射中使用的密钥的类型（或者更确切地说是它的签名，因为我们在文件中.mli），并且'a t是映射本身的（多态/抽象）类型。不过我想知道!+有什么用。我尝试寻找一些有关它的文档，但不幸的是没有找到任何文档。

如果可能的话，我希望得到有关此问题的解释和/或相关文档/教程的链接。

提前致谢。

在下面的代码中，我不确定我是否理解为什么_nested2.

这是否意味着只有顶级定义才能概括其推断类型以匹配显式多态签名？

let toplevel1 : 'a. 'a -> int = (fun _ -> 0)
let toplevel2 : 'a. 'a -> int = (fun (_ : 'a) -> 0)

let nest1 =
  let _nested1 : 'a. 'a -> int = (fun _ -> 0) in 0

let nest2 =
  let _nested2 : 'a. 'a -> int = (fun (_ : 'a) -> 0) in 0
(*                               ^^^^^^^^^^^^^^^^^^^
   Error: This definition has type 'a -> int which is less general …

我是 Coq 的新手，想知道以下内容之间有什么区别：

Class test (f g: nat -> nat) := {
  init:   f 0 = 0 /\ g 0 = 0;
  output: ...another proposition about f and g...;
}.

和

Class test := {
  f: nat -> nat;
  g: nat -> nat;
  init:   f 0 = 0 /\ g 0 = 0;
  output: ...another proposition about f and g...;
}.

有人能提供解释吗？

在 Coq 标准库中，“小于”关系对于自然数 ( lt_dec) 和整数 ( Z_lt_dec) 是可判定的。然而，当我搜索 ( Search ({ _ _ _ } + {~ _ _ _ })) 时，我找不到 aQ_le_dec或Qle_dec的有理数，只能Qeq_dec找到可判定的相等性。

这是因为“小于”关系对于 Coq 中的有理数来说是不可判定的吗？或者它是可以决定的，但决策过程没有在标准库中实现？

我的目标是扫描包含冒号作为除法的字符串，并将其两个部分保存在一个元组中。
例如：

input: "a:b"
output: ("a", "b")

到目前为止，我的方法不断收到错误消息：
“scanf：字符号 9 处输入错误：寻找 ':'，找到 '\n'”。

 Scanf.bscanf Scanf.Scanning.stdin "%s:%s" (fun x y -> (x,y));;

此外，我的方法适用于整数，我很困惑为什么它不适用于字符串。

Scanf.bscanf Scanf.Scanning.stdin "%d:%d" (fun x y -> (x,y));;
4:3
- : int * int = (4, 3)

给定一个从列表中删除连续重复项的函数

let rec compress l =
  match l with
  | [] -> []
  | [x] -> [x]
  | x :: (y :: _ as t) -> if x = y then compress t else x :: compress t;;

产生正确的结果

compress ["a"; "a";"b";"c";"c"] ;;
- : string list = ["a"; "b"; "c"]

但如果x :: (y :: _ as t)我改为x :: (y :: t)，那么我会得到不正确的结果

compress ["a"; "a";"b";"c";"c"] ;;
- : string list = ["b"; "c"]

这里发生了什么 ？我无法理解声明如何_ …

由于Coq有强大的类型推断算法，我想知道我们是否可以根据Notation的变量“重载”不同的重写符号。

作为一个例子，我将借用我在 Coq 中形式化类型化语言语义的一篇作品。在这种形式化中，我有类型对和表达式对，并且我想对它们各自的构造函数使用相同的符号：{ _ , _ }。

Inductive type: Type := ... | tpair: type -> type -> type | ...
Inductive expr: Type := ... | epair: expr -> expr -> expr | ... 

Notation "{ t1 , t2 }" := tpair t1 t2
Notation "{ e1 , e2 }" := epair e1 e2

我知道最后一个语句会引发错误，因为符号已经定义；如果有人考虑过围绕它进行欺骗，或者是否有另一种“官方”方式来做到这一点，我将不胜感激。