val while_cond_comp_typing
      (#g: env)
      (u: universe)
      (x: ppname)
      (ty inv_body: term)
      (inv_typing: tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_vprop)
    : Metatheory.comp_typing_u g (comp_while_cond x inv_body)
let while_cond_comp_typing (#g:env) (u:universe) (x:ppname) (ty:term) (inv_body:term)
                           (inv_typing:tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_vprop)
  : Metatheory.comp_typing_u g (comp_while_cond x inv_body)
  = Metatheory.admit_comp_typing g (comp_while_cond x inv_body)
val while_cond_comp_typing
      (#g: env)
      (u: universe)
      (x: ppname)
      (ty inv_body: term)
      (inv_typing: tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_vprop)
    : Metatheory.comp_typing_u g (comp_while_cond x inv_body)
let while_cond_comp_typing
      (#g: env)
      (u: universe)
      (x: ppname)
      (ty inv_body: term)
      (inv_typing: tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_vprop)
    : Metatheory.comp_typing_u g (comp_while_cond x inv_body) =
Metatheory.admit_comp_typing g (comp_while_cond x inv_body)
Pulse.Checker.While.fst.checked
Pulse.Typing.Metatheory.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.While.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.universe Pulse.Syntax.Base.ppname Pulse.Syntax.Base.term Pulse.Typing.tot_typing Pulse.Syntax.Base.tm_exists_sl Pulse.Typing.as_binder Pulse.Syntax.Base.tm_vprop Pulse.Typing.Metatheory.Base.admit_comp_typing Pulse.Typing.comp_while_cond Pulse.Typing.Metatheory.Base.comp_typing_u
module Pulse.Checker.While

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
module Metatheory = Pulse.Typing.Metatheory

let while_cond_comp_typing (#g:env) (u:universe) (x:ppname) (ty:term) (inv_body:term)
                           (inv_typing:tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_vprop)
val while_cond_comp_typing
      (#g: env)
      (u: universe)
      (x: ppname)
      (ty inv_body: term)
      (inv_typing: tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_vprop)
    : Metatheory.comp_typing_u g (comp_while_cond x inv_body)

    u7: Pulse.Syntax.Base.universe ->
    x: Pulse.Syntax.Base.ppname ->
    ty: Pulse.Syntax.Base.term ->
    inv_body: Pulse.Syntax.Base.term ->
    inv_typing:
      Pulse.Typing.tot_typing g
        (Pulse.Syntax.Base.tm_exists_sl u7 (Pulse.Typing.as_binder ty) inv_body)
        Pulse.Syntax.Base.tm_vprop
  -> Pulse.Typing.Metatheory.Base.comp_typing_u g (Pulse.Typing.comp_while_cond x inv_body)