代码之家 › 专栏 › 技术社区 › Daniel

如何在coq中为类型指定别名

coq typedef alias

Daniel · 技术社区 · 7 年前

假设我想在coq中创建一个自然数矩阵。

我有一个内置的coq列表,要创建一个自然数列表,我只需要写 list nat .

为了创建一个二维列表(即矩阵),我需要 list (list nat) .

我的问题是:与其写作 列表(list nat) ,我该怎么做才能让coq理解这个词呢 matrix 就像是 列表(list nat)

我试过了 Notation "matrix" := list (list nat) Notation "(matrix nat)" := (list (list nat)) 等等,但似乎什么都不管用。

1 回复 | 直到 7 年前

Tej Chajed 7 年前

你可以写一个定义: Definition matrix := list (list nat) . 定义应该只适用于大多数情况(例如,你仍然可以写 Definition foo : matrix := [nil] ,带有列表符号)。

Notation matrix := (list (list nat)) .

推荐文章

thanasissdr · 创建一个bash别名,其中输出是没有空格的串联

8 年前

Darkhydro · 如果不在命令行指定python2.7,我如何具体运行它?[已关闭]

8 年前

flix · 具有多个命令的Doxygen别名

8 年前

chu8 · MySQL是否按照写入的顺序执行查询?

8 年前

durilka · 在TypeScript中扩展联合类型别名?

8 年前

ThomasRones · t-sql——merge into语句中的表别名——这两个中哪一个更好,为什么?

8 年前

Asara · 命令不能用作别名

8 年前

showkey · 如何在alias中设置函数参数?

9 年前

omini data · sql:如何在具有别名的结果的两个值之间进行筛选

9 年前

Shubham Goyal · SQL重复列名

10 年前