val universe_to_string (n: nat) (u: universe) : Tot string (decreases u)
let rec universe_to_string (n:nat) (u:universe) 
  : Tot string (decreases u) =
  let open R in
  match inspect_universe u with
  | Uv_Unk -> "_"
  | Uv_Zero -> sprintf "%d" n
  | Uv_Succ u -> universe_to_string (n + 1) u
  | Uv_BVar x -> if n = 0 then sprintf "%d" x else sprintf "(%d + %d)" x n
  | Uv_Max us ->
    let r = "(max _)" in
    // sprintf "(max %s %s)" (universe_to_string 0 u0) (universe_to_string 0 u1) in
    if n = 0 then r else sprintf "%s + %d" r n
  | _ -> sprintf "<univ>"
val universe_to_string (n: nat) (u: universe) : Tot string (decreases u)
let rec universe_to_string (n: nat) (u: universe) : Tot string (decreases u) =
let open R in
match inspect_universe u with
| Uv_Unk -> "_"
| Uv_Zero -> sprintf "%d" n
| Uv_Succ u -> universe_to_string (n + 1) u
| Uv_BVar x -> if n = 0 then sprintf "%d" x else sprintf "(%d + %d)" x n
| Uv_Max us ->
  let r = "(max _)" in
  if n = 0 then r else sprintf "%s + %d" r n
| _ -> sprintf "<univ>"
Pulse.Syntax.Printer.fst.checked
Pulse.Syntax.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.String.fsti.checked FStar.Sealed.fsti.checked FStar.Reflection.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Syntax.Printer.fst
Prims.nat Pulse.Syntax.Base.universe FStar.Reflection.V2.Builtins.inspect_universe FStar.Printf.sprintf FStar.Reflection.Types.universe Pulse.Syntax.Printer.universe_to_string Prims.op_Addition Prims.op_Equality Prims.int Prims.bool Prims.string FStar.Reflection.V2.Data.universes FStar.Reflection.V2.Data.universe_view
module Pulse.Syntax.Printer
open FStar.Printf
open Pulse.Syntax.Base

module L = FStar.List.Tot

module T = FStar.Tactics.V2
module Un = FStar.Sealed
module R = FStar.Reflection.V2

let tot_or_ghost_to_string = function
  | T.E_Total -> "total"
  | T.E_Ghost -> "ghost"


let name_to_string (f:R.name) = String.concat "." f

let dbg_printing : bool = true

// let constant_to_string = function
//   | Unit -> "()"
//   | Bool true -> "true"
//   | Bool false -> "false"
//   | Int i -> sprintf "%d" i

let rec universe_to_string (n:nat) (u:universe)
val universe_to_string (n: nat) (u: universe) : Tot string (decreases u)
n: Prims.nat -> u6: Pulse.Syntax.Base.universe -> Prims.Tot Prims.string