val type_of_fv (g: env) (fv: R.fv) : T.Tac (option R.term)
let type_of_fv (g:env) (fv:R.fv)
  : T.Tac (option R.term)
  = let n = R.inspect_fv fv in
    match R.lookup_typ (fstar_env g) n with
    | None -> None
    | Some se ->
      match R.inspect_sigelt se with
      | R.Unk -> None
      | R.Sg_Let _ lbs -> (
        L.tryPick
          (fun lb -> 
            let lbv = R.inspect_lb lb in
            if R.inspect_fv lbv.lb_fv = n
            then Some lbv.lb_typ
            else None)
          lbs
      )
      | R.Sg_Val _ _ t -> Some t
      | R.Sg_Inductive _nm _univs params typ _ -> None
val type_of_fv (g: env) (fv: R.fv) : T.Tac (option R.term)
let type_of_fv (g: env) (fv: R.fv) : T.Tac (option R.term) =
let n = R.inspect_fv fv in
match R.lookup_typ (fstar_env g) n with
| None -> None
| Some se ->
  match R.inspect_sigelt se with
  | R.Unk -> None
  | R.Sg_Let _ lbs ->
    (L.tryPick (fun lb ->
            let lbv = R.inspect_lb lb in
            if R.inspect_fv lbv.lb_fv = n then Some lbv.lb_typ else None)
        lbs)
  | R.Sg_Val _ _ t -> Some t
  | R.Sg_Inductive _nm _univs params typ _ -> None
Pulse.Checker.Prover.Match.fst.checked
Pulse.Typing.Util.fsti.checked Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Checker.VPropEquiv.fsti.checked Pulse.Checker.Prover.Util.fsti.checked Pulse.Checker.Prover.Substs.fsti.checked Pulse.Checker.Prover.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.Prover.Match.fst
Pulse.Typing.Env.env FStar.Reflection.Types.fv FStar.Reflection.V2.Builtins.lookup_typ Pulse.Typing.Env.fstar_env FStar.Pervasives.Native.None FStar.Reflection.Types.term FStar.Reflection.Types.sigelt FStar.Reflection.V2.Builtins.inspect_sigelt Prims.bool Prims.list FStar.Reflection.Types.letbinding FStar.List.Tot.Base.tryPick FStar.Reflection.Types.typ Prims.op_Equality FStar.Reflection.Types.name FStar.Reflection.V2.Builtins.inspect_fv FStar.Reflection.V2.Data.__proj__Mklb_view__item__lb_fv FStar.Pervasives.Native.Some FStar.Reflection.V2.Data.__proj__Mklb_view__item__lb_typ FStar.Pervasives.Native.option FStar.Reflection.V2.Data.lb_view Prims.precedes FStar.Reflection.V2.Builtins.inspect_lb FStar.Reflection.Types.univ_name FStar.Reflection.Types.binders FStar.Reflection.V2.Data.ctor
module Pulse.Checker.Prover.Match

open Pulse.Syntax
open Pulse.Typing
open Pulse.Typing.Combinators
open Pulse.Typing.Metatheory
open Pulse.Typing.Util
open Pulse.Checker.VPropEquiv
open Pulse.Checker.Prover.Base
open Pulse.Checker.Prover.Util

module L = FStar.List.Tot
module R = FStar.Reflection.V2
module TermEq = FStar.Reflection.V2.TermEq
module T = FStar.Tactics.V2

module RUtil = Pulse.Reflection.Util
module P = Pulse.Syntax.Printer
module PS = Pulse.Checker.Prover.Substs

let equational (t:term) : bool =
  match t.t with
  | Tm_FStar host_term ->
    (match R.inspect_ln host_term with
     | R.Tv_Match _ _ _ -> true
     | _ -> false)
  | _ -> false

let type_of_fv (g:env) (fv:R.fv)
val type_of_fv (g: env) (fv: R.fv) : T.Tac (option R.term)
g: Pulse.Typing.Env.env -> fv: FStar.Reflection.Types.fv
  -> FStar.Tactics.Effect.Tac (FStar.Pervasives.Native.option FStar.Reflection.Types.term)