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_IntroPure? 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_IntroPure? t.term })

  : T.Tac (checker_result_t g pre post_hint) =

  let g = Pulse.Typing.Env.push_context g "check_intro_pure" t.range in

  let Tm_IntroPure { p } = t.term in
  let (| p, p_typing |) = check_prop g p in
  let pv = check_prop_validity g p p_typing in
  let st_typing = T_IntroPure _ _ p_typing pv in
  prove_post_hint (try_frame_pre pre_typing (match_comp_res_with_post_hint st_typing 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_IntroPure? 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_IntroPure? t.term})
    : T.Tac (checker_result_t g pre post_hint) =
let g = Pulse.Typing.Env.push_context g "check_intro_pure" t.range in
let Tm_IntroPure { p = p } = t.term in
let (| p , p_typing |) = check_prop g p in
let pv = check_prop_validity g p p_typing in
let st_typing = T_IntroPure _ _ p_typing pv in
prove_post_hint (try_frame_pre pre_typing
      (match_comp_res_with_post_hint st_typing post_hint)
      res_ppname)
  post_hint
  t.range
Pulse.Checker.IntroPure.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Env.fsti.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.IntroPure.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_IntroPure Pulse.Syntax.Base.__proj__Mkst_term__item__term Pulse.Typing.tm_prop 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_IntroPure Pulse.Syntax.Base.Mkst_term'__Tm_IntroPure__payload Pulse.Typing.comp_intro_pure Pulse.Typing.T_IntroPure Pulse.Typing.prop_validity Pulse.Checker.IntroPure.check_prop_validity Prims.dtuple2 Pulse.Checker.IntroPure.check_prop Pulse.Syntax.Base.st_term' Prims.eq2 Pulse.Typing.Env.push_context
module Pulse.Checker.IntroPure

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

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

let check_prop (g:env) (p:term) 
  : T.Tac (p:term & tot_typing g p tm_prop) =
  
  let p0 = p in
  let (| p, p_typing |) = Pulse.Checker.Pure.check_vprop g (tm_pure p) in
  match p.t with
  | Tm_Pure pp ->
    let prop_typing = Pulse.Typing.Metatheory.pure_typing_inversion #_ #pp p_typing in
    (| pp, prop_typing |)
  | _ ->
    fail g None
      (Printf.sprintf "Impossible: check_intro_pure: checking a pure vprop %s returned a non-pure vprop %s,\
                       please file a bug-report"
         (P.term_to_string (tm_pure p0))
         (P.term_to_string p))

let check_prop_validity (g:env) (p:term) (typing:tot_typing g p tm_prop): T.Tac (prop_validity g p) =
    Pulse.Checker.Pure.check_prop_validity g p typing

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_IntroPure? 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_IntroPure? 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_IntroPure? (Mkst_term?.term t)}
  -> FStar.Tactics.Effect.Tac (Pulse.Checker.Base.checker_result_t g pre post_hint)