val is_annotated_type_array (t: term) : option term
let is_annotated_type_array (t:term) : option term =
  match is_pure_app t with
  | Some (head, None, a) ->
    (match is_fvar head with
     | Some (l, _) ->
       if l = RU.array_lid
       then Some a
       else None
     | _ -> None 
    )

  | _ -> None
val is_annotated_type_array (t: term) : option term
let is_annotated_type_array (t: term) : option term =
match is_pure_app t with
| Some (head, None, a) ->
  (match is_fvar head with
    | Some (l, _) -> if l = RU.array_lid then Some a else None
    | _ -> None)
| _ -> None
Pulse.Checker.WithLocalArray.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.WithLocalArray.fst
Pulse.Syntax.Base.term Pulse.Syntax.Pure.is_pure_app Pulse.Syntax.Pure.is_fvar FStar.Reflection.Types.name Prims.list Pulse.Syntax.Base.universe Prims.op_Equality Prims.string Pulse.Reflection.Util.array_lid FStar.Pervasives.Native.Some Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.tuple3 Pulse.Syntax.Base.qualifier
module Pulse.Checker.WithLocalArray

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

module T = FStar.Tactics.V2
module P = Pulse.Syntax.Printer
module RU = Pulse.Reflection.Util

let extend_post_hint
  (g:env)
  (p:post_hint_for_env g)
  (init_t:term)
  (x:var { ~ (Set.mem x (dom g)) })
  : post_hint_for_env (push_binding g x ppname_default init_t)
  = { p with post = comp_withlocal_array_body_post p.post init_t (null_var x);
             post_typing = admit() } //star typing intro

let with_local_array_pre_typing (#g:env) (#pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (init_t:term)
  (init:term)
  (len:term)
  (init_typing:tot_typing g init init_t)
  (len_typing:tot_typing g len tm_szt)
  (x:var { ~ (Set.mem x (dom g)) })
  : tot_typing (push_binding g x ppname_default (mk_array init_t))
               (comp_withlocal_array_body_pre pre init_t (null_var x) init len)
               tm_vprop
  = admit()
val is_annotated_type_array (t: term) : option term
t: Pulse.Syntax.Base.term -> FStar.Pervasives.Native.option Pulse.Syntax.Base.term