我有一个问题: Record
和Definition
我有这个定义:
Definition rule := term -> term.
Run Code Online (Sandbox Code Playgroud)
我为它写了一个布尔函数.
Definition beq_rule a b := beq_term a && beq_term b.
Run Code Online (Sandbox Code Playgroud)
哪里 beq_term : term -> term -> bool.
所以我的beq_rule
实际定义返回的确切类型beq_term
不是我想要的.我希望它为我返回一个类型: rule -> rule -> bool.
所以我改变了规则的定义Record
:
Record rule := mkRule {lhs : term; rhs : term}.
Run Code Online (Sandbox Code Playgroud)
和
Definition beq_rule (a b : rule) : bool :=
beq_term (lhs a) (lhs b) && beq_term (rhs a) (rhs b).
Run Code Online (Sandbox Code Playgroud)
我的问题是:
1)我的第一次rule
使用Definition
和另一次使用之间有什么不同Record
?
2)如果我想定义规则,Definition
我可以在定义中给出别名lhs
和rhs
喜欢Record
吗?
你的两个定义rule
是完全不同的东西
Definition rule := term -> term
Run Code Online (Sandbox Code Playgroud)
将规则定义为Prop
函数类型的类型(或)别名term -> term
.于是
Definition not_what_you_meant : rule := fun t => t.
Run Code Online (Sandbox Code Playgroud)
很乐意编译.
至于Record
和之间的关系Definition
. Record
只是一个转换成一个宏的宏Inductive
.所以
Record rule := mkRule {lhs : term; rhs : term}.
Run Code Online (Sandbox Code Playgroud)
是相同的
Inductive rule := mkRule : term -> term -> rule.
Run Code Online (Sandbox Code Playgroud)
加上访问者功能
Definition lhs (r : rule) : term :=
match r with
mkRule l _ => l
end.
etc.
Run Code Online (Sandbox Code Playgroud)
你应该认为它与Inductive
根本不同Definition
. Definition
定义别名.另一种说法Definition
是"引用透明"的方式,你可以(最多可变重命名)总是用定义的右边替换其名称的任何出现.
Inductive
另一方面,通过列出一组构造函数来定义类型(Coqs Universe的元素).以更合乎逻辑的思维Inductive
方式,以确保"和谐"的方式根据其消除/引入规则定义逻辑命题.
归档时间: |
|
查看次数: |
2374 次 |
最近记录: |