val print_list_aux (f: ('a -> Tac string)) (xs: list 'a) : Tac string
let rec print_list_aux (f:'a -> Tac string) (xs:list 'a) : Tac string =
  match xs with
  | [] -> ""
  | [x] -> f x
  | x::xs -> f x ^ "; " ^ print_list_aux f xs
val print_list_aux (f: ('a -> Tac string)) (xs: list 'a) : Tac string
let rec print_list_aux (f: ('a -> Tac string)) (xs: list 'a) : Tac string =
match xs with
| [] -> ""
| [x] -> f x
| x :: xs -> f x ^ "; " ^ print_list_aux f xs
FStar.Tactics.Print.fst.checked
prims.fst.checked FStar.Tactics.V2.Derived.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.fsti.checked
FStar.Tactics.Print.fst
Prims.string Prims.list Prims.op_Hat FStar.Tactics.Print.print_list_aux
module FStar.Tactics.Print

open FStar.Reflection.V2
open FStar.Tactics.Effect
open FStar.Tactics.V2.Builtins
open FStar.Tactics.V2.Derived
open FStar.Tactics.NamedView

let namedv_to_string (x:namedv) : Tac string=
  unseal x.ppname ^ "#" ^ string_of_int x.uniq

private
let paren (s:string) : string = "(" ^ s ^ ")"

(* TODO: making this a local definition in print_list fails to extract. *)
private
val print_list_aux (f: ('a -> Tac string)) (xs: list 'a) : Tac string
f: (_: 'a -> FStar.Tactics.Effect.Tac Prims.string) -> xs: Prims.list 'a
  -> FStar.Tactics.Effect.Tac Prims.string