Replace lets by definitions in test example

src/LocalBlockchainTests.v

@@ -10,13 +10,13 @@ Import ListNotations.
 
 Section LocalBlockchainTests.
   (* Addresses *)
-  Let congress_1 := 1.
-  Let baker := 10.
-  Let person_1 := 11.
-  Let person_2 := 12.
-  Let person_3 := 13.
+  Definition congress_1 := 1.
+  Definition baker := 10.
+  Definition person_1 := 11.
+  Definition person_2 := 12.
+  Definition person_3 := 13.
 
-  Let chain1 :=
+  Definition chain1 :=
     initial_chain_builder LocalBlockchain.lc_builder_interface.
 
   Definition unpack_option {A : Type} (a : option A) :=
@@ -29,31 +29,31 @@ Section LocalBlockchainTests.
     end.
 
   (* Baker mines an empty block (and gets some coins) *)
-  Let chain2 : ChainBuilder :=
+  Definition chain2 : ChainBuilder :=
     unpack_option (chain1.(add_block) baker []).
 
   Compute (account_balance chain2 person_1).
   Compute (account_balance chain2 baker).
 
   (* Baker transfers 10 coins to person_1 *)
-  Let chain3 : ChainBuilder :=
+  Definition chain3 : ChainBuilder :=
     unpack_option (chain2.(add_block) baker [(baker, act_transfer person_1 10)]).
 
   Compute (account_balance chain3 person_1).
   Compute (account_balance chain3 baker).
 
   (* person_1 deploys a Congress contract *)
-  Let setup_rules :=
+  Definition setup_rules :=
     {| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
        margin_needed_permille := 501;
        debating_period_in_blocks := 0; |}.
 
-  Let setup := Congress.build_setup setup_rules.
+  Definition setup := Congress.build_setup setup_rules.
 
-  Let deploy_congress : ChainAction :=
+  Definition deploy_congress : ChainAction :=
     create_deployment 5 Congress.contract setup.
 
-  Let chain4 : ChainBuilder :=
+  Definition chain4 : ChainBuilder :=
     unpack_option (chain3.(add_block) baker [(person_1, deploy_congress)]).
 
   Compute (contract_deployment chain4 congress_1).
@@ -61,11 +61,11 @@ Section LocalBlockchainTests.
   Compute (account_balance chain4 baker).
   Compute (account_balance chain4 congress_1).
 
-  Let congress_ifc :=
+  Definition congress_ifc :=
     unpack_option
       (get_contract_interface chain4 congress_1 Congress.Setup Congress.Msg Congress.State).
 
-  Let congress_state chain : Congress.State :=
+  Definition congress_state chain : Congress.State :=
     match congress_ifc.(get_state) chain with
     | Some s => s
     | None => {| owner := 0;
@@ -79,10 +79,10 @@ Section LocalBlockchainTests.
   Compute (FMap.elements (congress_state chain4).(members)).
 
   (* person_1 adds person_1 and person_2 as members of congress *)
-  Let add_person p :=
+  Definition add_person p :=
     congress_ifc.(call) 0 (add_member p).
 
-  Let chain5 : ChainBuilder :=
+  Definition chain5 : ChainBuilder :=
     unpack_option
       (chain4.(add_block)
                 baker
@@ -93,29 +93,29 @@ Section LocalBlockchainTests.
 
   (* person_1 creates a proposal to send 3 coins to person_3 using funds
      of the contract *)
-  Let create_proposal_call :=
+  Definition create_proposal_call :=
     congress_ifc.(call) 0 (create_proposal [cact_transfer person_3 3]).
 
-  Let chain6 : ChainBuilder :=
+  Definition chain6 : ChainBuilder :=
     unpack_option (chain5.(add_block) baker [(person_1, create_proposal_call)]).
 
   Compute (FMap.elements (congress_state chain6).(proposals)).
 
   (* person_1 and person_2 vote for the proposal *)
-  Let vote_proposal :=
+  Definition vote_proposal :=
     congress_ifc.(call) 0 (vote_for_proposal 1).
 
-  Let chain7 : ChainBuilder :=
+  Definition chain7 : ChainBuilder :=
     unpack_option
       (chain6.(add_block) baker [(person_1, vote_proposal); (person_2, vote_proposal)]).
 
   Compute (FMap.elements (congress_state chain7).(proposals)).
 
   (* Person 3 finishes the proposal (anyone can finish it after voting) *)
-  Let finish_proposal :=
+  Definition finish_proposal :=
     congress_ifc.(call) 0 (finish_proposal 1).
 
-  Let chain8 : ChainBuilder :=
+  Definition chain8 : ChainBuilder :=
     unpack_option (chain7.(add_block) baker [(person_3, finish_proposal)]).
 
   Compute (FMap.elements (congress_state chain8).(proposals)).