Definition run_your_name_ok (argv : list LString.t) (name : LString.t)
  : Run.t (your_name argv) tt.
  eapply Run.Let. apply (Run.log_ok (LString.s "What is your name?")).
  eapply Run.Let. apply (Run.read_line_ok name).
  apply (Run.log_ok (_ ++ name ++ _)).
Defined.

Definition run_your_name_error (argv : list LString.t)
  : Run.t (your_name argv) tt.
  eapply Run.Let. apply (Run.log_ok (LString.s "What is your name?")).
  eapply Run.Let. apply Run.read_line_error.
  apply Run.Ret.
Defined.