printString in the printing example.

Author: gregory malecha

examples/Printing.v

@@ -11,9 +11,16 @@ Definition print {T : Type} {ST : Show T} (val : T) : PrinterMonad unit :=
   @MonadWriter.tell _ (@show_mon _ ShowScheme_string_compose) _ _
                     (@show _ ST val _ show_inj (@show_mon _ ShowScheme_string_compose)).
 
+Definition printString (str : string) : PrinterMonad unit :=
+  @MonadWriter.tell _ (@show_mon _ ShowScheme_string_compose) _ _
+                    (@show_exact str _ show_inj (@show_mon _ ShowScheme_string_compose)).
+
 Definition runPrinter {T : Type} (c : PrinterMonad T) : T * string :=
   let '(val,str) := unIdent (runWriterT c) in
   (val, str ""%string).
 
 
-Eval compute in runPrinter (Monad.bind (print 1) (fun _ => print 2)).
+Eval compute in runPrinter (Monad.bind (print 1) (fun _ => print 2)).
+
+Eval compute in runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)).
+Eval compute in runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)).