printString in the printing example.

coq-community · Jan 8, 2015 · ac569fb · ac569fb
1 parent bd1caa9
commit ac569fb
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/examples/Printing.v b/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)).