val from_show (#a: _) {| d: tac_showable a |} : printable a
let from_show #a {| d : tac_showable a |} : printable a = {
  pp = (fun x -> arbitrary_string (show x));
}
val from_show (#a: _) {| d: tac_showable a |} : printable a
let from_show #a {| d: tac_showable a |} : printable a =
{ pp = (fun x -> arbitrary_string (show x)) }
Pulse.PP.fst.checked
Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.Base.fsti.checked Pulse.Show.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Tactics.fst.checked FStar.Stubs.Pprint.fsti.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.PP.fst
Pulse.Show.tac_showable Pulse.PP.Mkprintable FStar.Stubs.Pprint.arbitrary_string FStar.Stubs.Pprint.document Prims.string Pulse.Show.show Pulse.PP.printable
module Pulse.PP

include FStar.Stubs.Pprint

open FStar.Tactics
open FStar.Tactics.Typeclasses
open FStar.Stubs.Pprint
open Pulse.Typing
open Pulse.Syntax.Base
open Pulse.Syntax.Printer

open Pulse.Show

(* A helper to create wrapped text *)
val text : string -> FStar.Stubs.Pprint.document
let text (s:string) : FStar.Stubs.Pprint.document =
  flow (break_ 1) (words s)

(* Nests a document 2 levels deep, as a block. It inserts a hardline
before the doc, so if you want to format something as

  hdr
    subdoc
  tail

  you should write  hdr ^^ indent (subdoc) ^/^ tail.  Note the ^^ vs ^/^.
*)
val indent : document -> document
let indent d =
  nest 2 (hardline ^^ align d)

class printable (a:Type) = {
  pp : a -> Tac document;
}

(* Repurposing a show instance *)
val from_show (#a: _) {| d: tac_showable a |} : printable a
{| d: Pulse.Show.tac_showable a |} -> Pulse.PP.printable a