(* The following defines the absolute name a.a *)

Definition a := 0.