let mk_arrow ty t = RT.mk_arrow (elab_term ty) T.Q_Explicit (elab_term t)
let mk_arrow ty t =
RT.mk_arrow (elab_term ty) T.Q_Explicit (elab_term t)
Pulse.Checker.Base.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.LN.fsti.checked Pulse.Typing.FV.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Syntax.Printer.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Checker.Pure.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.String.fsti.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Range.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.Ghost.fsti.checked
Pulse.Checker.Base.fst
Pulse.Syntax.Base.term FStar.Reflection.Typing.mk_arrow Pulse.Elaborate.Pure.elab_term FStar.Reflection.V2.Data.Q_Explicit FStar.Reflection.Types.term
module Pulse.Checker.Base

module T = FStar.Tactics.V2
module RT = FStar.Reflection.Typing
module Metatheory = Pulse.Typing.Metatheory
module CP = Pulse.Checker.Pure
module RU = Pulse.RuntimeUtils
module FV = Pulse.Typing.FV
module P = Pulse.Syntax.Printer

open Pulse.Typing.Combinators
open Pulse.Typing.Metatheory

let format_failed_goal (g:env) (ctxt:list term) (goal:list term) =
  let terms_to_strings (ts:list term)= T.map Pulse.Syntax.Printer.term_to_string ts in
  let numbered_list ss = 
       let _, s = T.fold_left (fun (i, acc) s -> (i+1, Printf.sprintf "%d. %s" i s :: acc)) (1, []) ss in
       String.concat "\n  " (List.rev s)
  in
  let format_terms (ts:list term) = numbered_list (terms_to_strings ts) in
  Printf.sprintf 
    "Failed to prove the following goals:\n  \
     %s\n\
     The remaining conjuncts in the separation logic context available for use are:\n  \
     %s\n\
     The typing context is:\n  \
     %s\n"
    (format_terms goal)
    (format_terms ctxt)
    (env_to_string g)
val mk_arrow : ty: Pulse.Syntax.Base.term -> t: Pulse.Syntax.Base.term -> FStar.Reflection.Types.term
ty: Pulse.Syntax.Base.term -> t: Pulse.Syntax.Base.term -> FStar.Reflection.Types.term