val is_term_an_invocation_of_function (t fn: term) (argc: nat) : Tac bool
val is_term_an_invocation_of_function (t fn: term) (argc: nat) : Tac bool
let rec is_term_an_invocation_of_function (t: term) (fn: term) (argc: nat) : Tac bool =
  if argc = 0 then
    term_eq t fn
  else
    match t with
    | Tv_App fn' arg -> is_term_an_invocation_of_function fn' fn (argc - 1)
    | _ -> false
module Util.Tactics

open FStar.Printf
open FStar.Tactics.V2
open FStar.Reflection.V2.TermEq

/// Replacing a function in the current goal
///
/// Using the tactic `replace_fn_in_goal` will replace all instances
/// of a given function invocation in the goal with an invocation of
/// another function.  You give it the name of the function to be
/// replaced (`fn`), the number of arguments to that function
/// (`argc`), and a lemma that demonstrates that the function is
/// equivalent to another function (`lem`).  That lemma must take
/// `argc` arguments and have a postcondition that says that `fn`
/// applied to that many arguments is `==` to another function.  You
/// don't have to supply the name of that second function since it's
/// taken from that postcondition automatically.
///
/// NOTE: The lemma must have as a postcondition that f a1 a2 ... ==
/// f' a1 a2 where f is the replaced function.  If it says that f' a1
/// a2 ... == f a1 a2 instead (i.e., in the wrong order) then
/// `replace_fn_in_goal` won't work.
/
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Util.Tactics.fst
t: FStar.Tactics.NamedView.term -> fn: FStar.Tactics.NamedView.term -> argc: Prims.nat
  -> FStar.Tactics.Effect.Tac Prims.bool
FStar.Tactics.NamedView.term Prims.nat Prims.op_Equality Prims.int FStar.Reflection.V2.TermEq.term_eq Prims.bool FStar.Stubs.Reflection.V2.Data.argv Util.Tactics.is_term_an_invocation_of_function Prims.op_Subtraction FStar.Tactics.NamedView.named_term_view FStar.Tactics.NamedView.inspect
let rec is_term_an_invocation_of_function (t fn: term) (argc: nat) : Tac bool =
  
if argc = 0
then term_eq t fn
else
  match t with
  | Tv_App fn' arg -> is_term_an_invocation_of_function fn' fn (argc - 1)
  | _ -> false