0

我正在尝试在 Coq 中模拟全局和局部变量，但我什至不知道如何开始。有没有人可以给我一个提示或一些建议？我阅读了很多关于这种编程语言的文档，但我无法弄清楚。先感谢您！

4

1 回答 1

1

这取决于“本地”和“全球”的含义。Coq 中的变量与大多数编程语言的工作方式不同，因为它们不能被修改。最接近全局变量的是顶级定义，最接近局部变量的是局部定义：

Definition i_am_a_global : nat := 42.

Definition my_function (my_parameter : nat) : nat :=
  (* Function parameters are always local *)
  let my_local := my_parameter + my_parameter in
  my_local + i_am_a_global.
于 2020-12-17T17:10:52.987 回答