val print_st_typing (#g #t #c: _) (d: st_typing g t c) : T.Tac string
let rec print_st_typing #g #t #c (d:st_typing g t c)
  : T.Tac string 
  = match d with
    | T_Abs g x q b u body c tt body_typing ->
      Printf.sprintf "(T_Abs ... %s)" (print_st_typing body_typing)
    
    | T_STApp _ _ _ _ _ _ _ _ ->
      "T_STApp"
    
    | T_Return _ _ _ _ _ _ _ _ _ _ _ ->
      "T_Return"

    | T_Lift _ _ _ _ d _ ->
      Printf.sprintf "(T_Lift %s)" (print_st_typing d)

    | T_Bind g e1 e2 c1 c2 b x c d1 _ d2 _ ->
      Printf.sprintf "(T_Bind %s %s)" (print_st_typing d1) (print_st_typing d2)

    | T_TotBind g e1 e2 t1 c2 b x _ d ->
      Printf.sprintf "(T_TotBind %s)" (print_st_typing d)

    | T_Frame g e c frame _ body ->
      Printf.sprintf "(T_Frame %s %s)" (Pulse.Syntax.Printer.term_to_string frame) (print_st_typing body)

    | T_If _ _ _ _ _ _ _ _ _ _ _ ->
      "T_If"

    | T_Match _ _ _ _ _ _ _ _ _ _ ->
      "T_Match"

    | T_Equiv g e c c' d eq ->
      Printf.sprintf "(T_Equiv %s)"
         (print_st_typing d)
    //   Printf.sprintf "(T_Equiv \n\t{%s}\n\t{%s}\n\t %s)"
    //      (Pulse.Syntax.Printer.comp_to_string c)
    //      (Pulse.Syntax.Printer.comp_to_string c')
    //      (print_st_typing d)
        
    | T_IntroPure _ _ _ _ ->
      "T_IntroPure"

    | T_Rewrite _ _ _ _ _ ->
      "T_Rewrite"
      
    | _ -> "<UNK>"
val print_st_typing (#g #t #c: _) (d: st_typing g t c) : T.Tac string
let rec print_st_typing #g #t #c (d: st_typing g t c) : T.Tac string =
match d with
| T_Abs g x q b u body c tt body_typing ->
  Printf.sprintf "(T_Abs ... %s)" (print_st_typing body_typing)
| T_STApp _ _ _ _ _ _ _ _ -> "T_STApp"
| T_Return _ _ _ _ _ _ _ _ _ _ _ -> "T_Return"
| T_Lift _ _ _ _ d _ -> Printf.sprintf "(T_Lift %s)" (print_st_typing d)
| T_Bind g e1 e2 c1 c2 b x c d1 _ d2 _ ->
  Printf.sprintf "(T_Bind %s %s)" (print_st_typing d1) (print_st_typing d2)
| T_TotBind g e1 e2 t1 c2 b x _ d -> Printf.sprintf "(T_TotBind %s)" (print_st_typing d)
| T_Frame g e c frame _ body ->
  Printf.sprintf "(T_Frame %s %s)"
    (Pulse.Syntax.Printer.term_to_string frame)
    (print_st_typing body)
| T_If _ _ _ _ _ _ _ _ _ _ _ -> "T_If"
| T_Match _ _ _ _ _ _ _ _ _ _ -> "T_Match"
| T_Equiv g e c c' d eq -> Printf.sprintf "(T_Equiv %s)" (print_st_typing d)
| T_IntroPure _ _ _ _ -> "T_IntroPure"
| T_Rewrite _ _ _ _ _ -> "T_Rewrite"
| _ -> "<UNK>"
Pulse.Typing.Printer.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked
Pulse.Typing.Printer.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.st_term Pulse.Syntax.Base.comp Pulse.Typing.st_typing Pulse.Syntax.Base.var Prims.b2t FStar.Pervasives.Native.uu___is_None Pulse.Syntax.Base.typ Pulse.Typing.Env.lookup FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier Pulse.Syntax.Base.binder Pulse.Syntax.Base.universe Prims.l_not FStar.Set.mem Pulse.Syntax.Naming.freevars_st Pulse.Typing.tot_typing Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ty Pulse.Syntax.Pure.tm_type Pulse.Typing.Env.push_binding Pulse.Syntax.Base.ppname_default Pulse.Syntax.Naming.open_st_term_nv FStar.Pervasives.Native.Mktuple2 Pulse.Syntax.Base.ppname Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ppname FStar.Printf.sprintf Prims.string Pulse.Typing.Printer.print_st_typing Pulse.Syntax.Base.term Pulse.Syntax.Base.comp_st Pulse.Syntax.Pure.tm_arrow Pulse.Typing.as_binder Pulse.Syntax.Base.ctag Prims.bool Prims.l_and Pulse.Syntax.Naming.freevars Pulse.Typing.universe_of Pulse.Syntax.Naming.open_term Pulse.Syntax.Base.tm_vprop Pulse.Typing.lift_comp Prims.eq2 Pulse.Syntax.Base.comp_res Pulse.Syntax.Base.comp_u Pulse.Typing.bind_comp Pulse.Syntax.Base.v_as_nv Pulse.Syntax.Printer.term_to_string FStar.Set.union Pulse.Typing.tm_bool Pulse.Typing.mk_eq2 Pulse.Syntax.Pure.u0 Pulse.Typing.tm_true Pulse.Typing.tm_false Pulse.Typing.my_erased Pulse.Typing.comp_typing Prims.list FStar.Pervasives.Native.tuple2 Pulse.Syntax.Base.pattern Pulse.Typing.brs_typing Pulse.Typing.pats_complete FStar.List.Tot.Base.map FStar.Reflection.V2.Data.pattern Pulse.Elaborate.Pure.elab_pat Pulse.Typing.st_equiv Pulse.Typing.tm_prop Pulse.Typing.prop_validity Pulse.Syntax.Base.vprop Pulse.Typing.vprop_equiv
module Pulse.Typing.Printer
module T = FStar.Tactics
open Pulse.Syntax.Printer
open Pulse.Typing


#push-options "--query_stats --ifuel 1 --z3rlimit_factor 4 --split_queries no"
let rec print_st_typing #g #t #c (d:st_typing g t c)
val print_st_typing (#g #t #c: _) (d: st_typing g t c) : T.Tac string
d: Pulse.Typing.st_typing g t c -> FStar.Tactics.Effect.Tac Prims.string