val is_smt_fallback (t: R.term) : bool
let is_smt_fallback (t:R.term) : bool =
  match R.inspect_ln t with
  | R.Tv_FVar fv ->
    let name = R.inspect_fv fv in
    name = ["Steel";"Effect";"Common";"smt_fallback"]
  | _ -> false
val is_smt_fallback (t: R.term) : bool
let is_smt_fallback (t: R.term) : bool =
match R.inspect_ln t with
| R.Tv_FVar fv ->
  let name = R.inspect_fv fv in
  name = ["Steel"; "Effect"; "Common"; "smt_fallback"]
| _ -> false
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
FStar.Reflection.Types.term FStar.Reflection.V2.Builtins.inspect_ln FStar.Reflection.Types.fv Prims.op_Equality Prims.list Prims.string Prims.Cons Prims.Nil FStar.Reflection.Types.name FStar.Reflection.V2.Builtins.inspect_fv FStar.Reflection.V2.Data.term_view Prims.bool
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)
  : 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 is_smt_fallback (t: R.term) : bool
t: FStar.Reflection.Types.term -> Prims.bool