val arrow_of_abs (t: st_term{Tm_Abs? t.term}) : T.Tac term
let rec arrow_of_abs (t:st_term { Tm_Abs? t.term })
  : T.Tac term
  = let Tm_Abs { b; q; ascription; body } = t.term in
    if Tm_Abs? body.term
    then (
      let arr = arrow_of_abs body in
      tm_arrow b q (C_Tot arr)
    )
    else
      tm_arrow b q ascription
val arrow_of_abs (t: st_term{Tm_Abs? t.term}) : T.Tac term
let rec arrow_of_abs (t: st_term{Tm_Abs? t.term}) : T.Tac term =
let Tm_Abs { b = b ; q = q ; ascription = ascription ; body = body } = t.term in
if Tm_Abs? body.term
then
  (let arr = arrow_of_abs body in
    tm_arrow b q (C_Tot arr))
else tm_arrow b q ascription
Pulse.Checker.Abs.fst.checked
Pulse.Typing.FV.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.Abs.fst
Pulse.Syntax.Base.st_term Prims.b2t Pulse.Syntax.Base.uu___is_Tm_Abs Pulse.Syntax.Base.__proj__Mkst_term__item__term Pulse.Syntax.Base.binder FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier Pulse.Syntax.Base.comp Pulse.Syntax.Pure.tm_arrow Pulse.Syntax.Base.C_Tot Pulse.Syntax.Base.term Pulse.Checker.Abs.arrow_of_abs Prims.bool Pulse.Syntax.Base.st_term'
module Pulse.Checker.Abs

module T = FStar.Tactics.V2

open Pulse.Syntax
open Pulse.Typing
open Pulse.Typing.Combinators
open Pulse.Checker.Pure
open Pulse.Checker.Base

module P = Pulse.Syntax.Printer
module FV = Pulse.Typing.FV
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
(* Infers the the type of the binders from the specification alone, not the body *)

let rec arrow_of_abs (t:st_term { Tm_Abs? t.term })
val arrow_of_abs (t: st_term{Tm_Abs? t.term}) : T.Tac term
t: Pulse.Syntax.Base.st_term{Tm_Abs? (Mkst_term?.term t)}
  -> FStar.Tactics.Effect.Tac Pulse.Syntax.Base.term