val format_failed_goal (g:env) (ctxt:list term) (goal:list term) : T.Tac string
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 format_failed_goal (g:env) (ctxt:list term) (goal:list term) : T.Tac string
let format_failed_goal (g: env) (ctxt 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\nThe remaining conjuncts in the separation logic context available for use are:\n  %s\nThe typing context is:\n  %s\n"
  (format_terms goal)
  (format_terms ctxt)
  (env_to_string g)
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.Typing.Env.env Prims.list Pulse.Syntax.Base.term Prims.string FStar.Printf.sprintf Pulse.Typing.Env.env_to_string Prims.int FStar.String.concat FStar.List.Tot.Base.rev FStar.Pervasives.Native.tuple2 FStar.Tactics.Util.fold_left FStar.Pervasives.Native.Mktuple2 Prims.op_Addition Prims.Cons Prims.Nil FStar.Tactics.Util.map Pulse.Syntax.Printer.term_to_string
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
val format_failed_goal (g:env) (ctxt:list term) (goal:list term) : T.Tac string

    g: Pulse.Typing.Env.env ->
    ctxt: Prims.list Pulse.Syntax.Base.term ->
    goal: Prims.list Pulse.Syntax.Base.term
  -> FStar.Tactics.Effect.Tac Prims.string