val check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term { Tm_Rewrite? t.term })
  : T.Tac (checker_result_t g pre post_hint)
let check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_Rewrite? t.term})

  : T.Tac (checker_result_t g pre post_hint) =

  let g = push_context "check_rewrite" t.range g in
  let Tm_Rewrite {t1=p; t2=q} = t.term in
  let (| p, p_typing |) = check_vprop g p in
  let (| q, q_typing |) = check_vprop g q in
  let equiv_p_q =
      if eq_tm p q
      then VE_Refl g p
      else let elab_p = elab_term p in
           let elab_q = elab_term q in
           let res, issues = T.check_equiv (elab_env g) elab_p elab_q in
           T.log_issues issues;
           match res with
           | None -> 
             fail g (Some t.range)
                    (Printf.sprintf "rewrite: could not prove equality of %s and %s\nElaborations: %s and %s\n" 
                           (P.term_to_string p)
                           (P.term_to_string q)
                           (T.term_to_string elab_p)
                           (T.term_to_string elab_q))
           | Some token ->
            VE_Ext g p q token in
	let d = T_Rewrite _ p q p_typing equiv_p_q in
	prove_post_hint (try_frame_pre pre_typing (match_comp_res_with_post_hint d post_hint) res_ppname) post_hint t.range
val check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term { Tm_Rewrite? t.term })
  : T.Tac (checker_result_t g pre post_hint)
let check
      (g: env)
      (pre: term)
      (pre_typing: tot_typing g pre tm_vprop)
      (post_hint: post_hint_opt g)
      (res_ppname: ppname)
      (t: st_term{Tm_Rewrite? t.term})
    : T.Tac (checker_result_t g pre post_hint) =
let g = push_context "check_rewrite" t.range g in
let Tm_Rewrite { t1 = p ; t2 = q } = t.term in
let (| p , p_typing |) = check_vprop g p in
let (| q , q_typing |) = check_vprop g q in
let equiv_p_q =
  if eq_tm p q
  then VE_Refl g p
  else
    let elab_p = elab_term p in
    let elab_q = elab_term q in
    let res, issues = T.check_equiv (elab_env g) elab_p elab_q in
    T.log_issues issues;
    match res with
    | None ->
      fail g
        (Some t.range)
        (Printf.sprintf "rewrite: could not prove equality of %s and %s\nElaborations: %s and %s\n"
            (P.term_to_string p)
            (P.term_to_string q)
            (T.term_to_string elab_p)
            (T.term_to_string elab_q))
    | Some token -> VE_Ext g p q token
in
let d = T_Rewrite _ p q p_typing equiv_p_q in
prove_post_hint (try_frame_pre pre_typing (match_comp_res_with_post_hint d post_hint) res_ppname)
  post_hint
  t.range
Pulse.Checker.Rewrite.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.Rewrite.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.tot_typing Pulse.Syntax.Base.tm_vprop Pulse.Typing.post_hint_opt Pulse.Syntax.Base.ppname Pulse.Syntax.Base.st_term Prims.b2t Pulse.Syntax.Base.uu___is_Tm_Rewrite Pulse.Syntax.Base.__proj__Mkst_term__item__term Pulse.Checker.Prover.prove_post_hint Pulse.Syntax.Base.__proj__Mkst_term__item__range Pulse.Checker.Base.checker_result_t FStar.Pervasives.Native.None Pulse.Typing.post_hint_t Pulse.Checker.Prover.try_frame_pre FStar.Pervasives.dtuple3 Pulse.Syntax.Base.comp_st Pulse.Typing.st_typing Pulse.Checker.Base.match_comp_res_with_post_hint Pulse.Typing.wtag FStar.Pervasives.Native.Some Pulse.Syntax.Base.ctag Pulse.Syntax.Base.STT_Ghost Pulse.Syntax.Base.Tm_Rewrite Pulse.Syntax.Base.Mkst_term'__Tm_Rewrite__payload Pulse.Typing.comp_rewrite Pulse.Typing.T_Rewrite Pulse.Typing.vprop_equiv Pulse.Syntax.Base.eq_tm Pulse.Typing.VE_Refl Prims.bool FStar.Pervasives.Native.option FStar.Tactics.Types.equiv_token Pulse.Typing.elab_env FStar.Tactics.Types.issues Pulse.Typing.Env.fail Pulse.Syntax.Base.range Prims.string FStar.Printf.sprintf Pulse.Syntax.Printer.term_to_string FStar.Tactics.V2.Builtins.term_to_string Pulse.Typing.VE_Ext Prims.unit FStar.Tactics.V2.Builtins.log_issues FStar.Pervasives.Native.tuple2 FStar.Tactics.V2.Builtins.check_equiv FStar.Tactics.V2.Builtins.ret_t FStar.Reflection.Types.term Pulse.Elaborate.Pure.elab_term Prims.dtuple2 Pulse.Checker.Pure.check_vprop Pulse.Syntax.Base.st_term' Prims.eq2 Pulse.Checker.Pure.push_context
module Pulse.Checker.Rewrite

open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Pure
open Pulse.Checker.Base
open Pulse.Checker.Prover

module T = FStar.Tactics.V2
module P = Pulse.Syntax.Printer

let check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_Rewrite? t.term})
val check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term { Tm_Rewrite? t.term })
  : T.Tac (checker_result_t g pre post_hint)

    g: Pulse.Typing.Env.env ->
    pre: Pulse.Syntax.Base.term ->
    pre_typing: Pulse.Typing.tot_typing g pre Pulse.Syntax.Base.tm_vprop ->
    post_hint: Pulse.Typing.post_hint_opt g ->
    res_ppname: Pulse.Syntax.Base.ppname ->
    t: Pulse.Syntax.Base.st_term{Tm_Rewrite? (Mkst_term?.term t)}
  -> FStar.Tactics.Effect.Tac (Pulse.Checker.Base.checker_result_t g pre post_hint)