在精益中创建固定点的Coq 'fix‘关键字的等价物是什么
在精益中创建固定点的Coq 'fix‘关键字的等价物是什么
提问于 2020-03-29 18:45:39
我正在尝试将Coq术语直译为精益术语，但我意识到我不知道如何翻译Coq原语fix，如下所示：
Definition Fac : nat -> nat :=
fix f (n:nat) : nat :=
match n with
| 0 => 1
| S p => S p * f p
end.我不是问如何在归纳类型上定义递归函数，这在精益文档中有很好的解释，但我问的是如何定义“递归let”，即其主体调用自身的lambda抽象。我假设Lean中存在一个等价的原语。
谢谢。
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-03-30 00:38:11
有一个关于这个here的讨论。据我所知，没有很好的符号来表示它。
你能得到的最接近的方法是直接使用nat的递归器，或者直接使用well_founded.fix。
e.g
def fact (n : ℕ) : ℕ :=
let f : ℕ → ℕ := λ n, nat.rec_on n 1 (λ n fact, (n + 1) * fact) in
f n或
def fact' (n : ℕ) : ℕ :=
let f : ℕ → ℕ := λ n, well_founded.fix nat.lt_wf
(λ n fact, show ℕ, from nat.cases_on n (λ _, 1)
(λ n fact, (n + 1) * fact n n.lt_succ_self) fact)
n in
f n页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/60913060
复制相关文章
相似问题
腾讯云开发者
