我是 Coq 的新手,只是想弄清楚基本语法。如何向 let
添加多个子句?这是我正在尝试编写的函数:
Definition split {A:Set} (lst:list A) :=
let
fst := take (length lst / 2) lst
snd := drop (length lst / 2) lst
in (fst, snd) end.
这是错误:
Syntax error: 'in' expected after [constr:operconstr level 200] (in [constr:binder_constr]).
我想它需要在 fst
定义之后有一个 in
?
最佳答案
确实,您需要在第一个标识符之后in
。根据引用手册(§1.2.12):
let ident := term1 in term2
denotes the local binding ofterm1
to the variableident
interm2
.
您需要多个(嵌套)let ... in
表达式:
Definition split {A:Set} (lst:list A) :=
let fst := take (length lst / 2) lst in
let snd := drop (length lst / 2) lst in
(fst, snd).
<小时/>
顺便说一句,您可以使用标准库 ( List
module ) 中的 firstn
和 skipn
函数来代替 take
和 删除
:
Require Import Coq.Lists.List.
Import ListNotations.
Compute firstn 3 [1;2;3;4;5]. (* Result: [1;2;3] *)
Compute skipn 3 [1;2;3;4;5]. (* Result: [4;5] *)
这(以及一点点重构)产生了以下 split
定义(我将其重命名以避免遮蔽 split
标准函数):
Definition split_in_half {A:Set} (lst:list A) :=
let l2 := Nat.div2 (length lst) in
(firstn l2 lst, skipn l2 lst).
Compute split_in_half [1;2;3;4;5]. (* Result: ([1; 2], [3; 4; 5]) *)
顺便说一句,如果您担心多次传递输入列表,它仍然有很大的改进空间。如果您打算进行提取,例如,您可能会这样做。进入 OCaml。
关于syntax-error - Coq let 子句中的多个赋值,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40255709/