Inductive halt : Set :=
  | Halt
  | HContinue
  .
