Simulation of global and local variables in Coq

Question

I'm trying to simulate global and local variables in Coq, but I don't even know how to start. Is there anybody that can give me a hint or some pieces of advice? I read a lot of documentation about this programming language, but I can't figure it out. Thank you in advance!

Answer 1

It depends on what you mean by "local" and "global". Variables in Coq work differently from most programming languages, because they cannot be modified. The closest thing to a global variable is a top-level definition, and the closest thing to a local variable would be a local definition:

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.