如何在 Coq 中将字符串解析为列表列表？

Question

我试图将带有双换行符的字符串解析为 Coq 中的 int 列表列表，但我无法使其按预期工作。

示例字符串：

1
2

3
4

上面的字符串需要解析成

[[1; 2]; [3; 4]]

。 我按照similar example进行解析，但我认为我使用了错误的解析级别。

这是我的错误代码：

From Coq Require Export List NArith.

#[global] Open Scope N.
Import ListNotations.

Declare Custom Entry elfEntry.
Declare Custom Entry elfEntry1.

Notation "'input' elf1 .. elfN" :=
    (cons elf1 .. (cons elfN nil) ..)
  (at level 200, elf1 custom elfEntry, only parsing).

Notation "cal1 .. calN" := (cons cal1 .. (cons calN nil) ..)
  (in custom elfEntry at level 1, cal1 custom elfEntry1).

Notation "cal1" := cal1
  (in custom elfEntry1 at level 1, cal1 constr at level 1).

Definition example := input
1
2

3
4
.

Print example.

Answer 1

恐怕你需要一个明确的分隔符

Notation "'input' elf1 ';' .. ';' elfN" :=
    (cons elf1 .. (cons elfN nil) ..)
  (at level 200, elf1 custom elfEntry, only parsing).

Notation "cal1 .. calN" := (cons cal1 .. (cons calN nil) ..)
  (in custom elfEntry at level 1, cal1 custom elfEntry1).

Notation "cal1" := cal1
  (in custom elfEntry1 at level 1, cal1 constr at level 1).

Definition example := input
1
2
;
3
4
.

Print example.