val qual_to_string (q:option qualifier) : string
let qual_to_string = function
  | None -> ""
  | Some Implicit -> "#"
val qual_to_string (q:option qualifier) : string
let qual_to_string =
function
| None -> ""
| Some Implicit -> "#"
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
FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier Prims.string
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) 
  : 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 qual_to_string (q:option qualifier) : string
q: FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier -> Prims.string