Simulation of global and local variables in Coq

401 views Asked by At

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!

1

There are 1 answers

5
Arthur Azevedo De Amorim On

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.