Coq Syntax Highlighting Test

Inductive bool : Set :=
  | true : bool
  | false : bool.
(** just update (whether there is a value of not) *)
Definition update_local (LOC: list Local) (id: ident) (a: expr_val) : list Local :=
    if Find_in_Local LOC id then 
      let LOC' := Change_Local LOC id a in
        LOC'
    else 
      let LOC' := Insert_Local LOC id a in
        LOC'
.

(** if there is a memory block storing some value, update it *)
Definition update_sep cenv (venv: AbsTypeEnv) SEP (addr: expr_val) (a: expr_val) (a_ty: type) : option (list Separation) :=
    match Get_val_addr_in_sepx SEP addr with
    | Some (e, ty) =>
      if eqb_type ty a_ty then
        match typeof_exprVal cenv venv e with
        | Some t => if type_type_sim t ty then
                      let SEP' := Change_Sep SEP addr a in
                        Some SEP'
                    else None
        | None => None
        end
      else None
    | None => None
    end
.

#include <iostream>
using namespace std;
int main() {
    cout << "Hello, World!" << endl;
    return 0;
}