val lookup (g: env) (x: var) : option typ
let lookup (g:env) (x:var) : option typ =
  let m = as_map g in
  if Map.contains m x then Some (Map.sel m x) else None
val lookup (g: env) (x: var) : option typ
let lookup (g: env) (x: var) : option typ =
let m = as_map g in
if Map.contains m x then Some (Map.sel m x) else None
Pulse.Typing.Env.fsti.checked
Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Result.fsti.checked FStar.Stubs.Pprint.fsti.checked FStar.Set.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.Issue.fsti.checked
Pulse.Typing.Env.fsti
Pulse.Typing.Env.env Pulse.Syntax.Base.var FStar.Map.contains Pulse.Syntax.Base.typ FStar.Pervasives.Native.Some FStar.Map.sel Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option FStar.Map.t Pulse.Typing.Env.as_map
module Pulse.Typing.Env

open FStar.List.Tot

open Pulse.Syntax

module L = FStar.List.Tot

module RT = FStar.Reflection.Typing
module T = FStar.Tactics.V2
module Pprint = FStar.Stubs.Pprint

type binding = var & typ
type env_bindings = list binding

val env : Type0

val fstar_env (g:env) : RT.fstar_top_env

//
// most recent binding at the head of the list
//
val bindings (g:env) : env_bindings

val as_map (g:env) : Map.t var typ

let is_related_to (bs:list (var & typ)) (m:Map.t var typ) =
  (forall (b:var & typ).{:pattern L.memP b bs}
          L.memP b bs ==> (Map.contains m (fst b) /\
                           Map.sel m (fst b) == snd b)) /\
  
  (forall (x:var).{:pattern Map.contains m x} Map.contains m x ==> (L.memP (x, Map.sel m x) bs))

val bindings_as_map (g:env)
  : Lemma (bindings g `is_related_to` as_map g)
          [SMTPat (bindings g); SMTPat (as_map g)]

let dom (g:env) : Set.set var = Map.domain (as_map g)

let equal (g1 g2:env) =
  fstar_env g1 == fstar_env g2 /\
  bindings g1 == bindings g2

val equal_elim (g1 g2:env)
  : Lemma (requires equal g1 g2)
          (ensures g1 == g2)
          [SMTPat (equal g1 g2)]

val mk_env (f:RT.fstar_top_env) : g:env { fstar_env g == f }

val mk_env_bs (f:RT.fstar_top_env)
  : Lemma (bindings (mk_env f) == [])
          [SMTPat (bindings (mk_env f))]

val mk_env_dom (f:RT.fstar_top_env)
  : Lemma (dom (mk_env f) == Set.empty)
          [SMTPat (dom (mk_env f))]

val push_binding (g:env) (x:var { ~ (Set.mem x (dom g)) }) (n:ppname) (t:typ)
  : g':env { fstar_env g' == fstar_env g }

let singleton_env (f:_) (x:var) (t:typ) = push_binding (mk_env f) x ppname_default t

let push_binding_def (g:env) (x:var { ~ (Set.mem x (dom g)) }) (t:typ)
  = push_binding g x ppname_default t

val push_binding_bs (g:env) (x:var { ~ (Set.mem x (dom g)) }) (n:ppname) (t:typ)
  : Lemma (bindings (push_binding g x n t) == (x, t) :: bindings g)
          [SMTPat (bindings (push_binding g x n t))]

val push_binding_as_map (g:env) (x:var { ~ (Set.mem x (dom g)) }) (n:ppname) (t:typ)
  : Lemma (as_map (push_binding g x n t) == Map.upd (as_map g) x t)
          [SMTPat (as_map (push_binding g x n t))]
val lookup (g: env) (x: var) : option typ
g: Pulse.Typing.Env.env -> x: Pulse.Syntax.Base.var
  -> FStar.Pervasives.Native.option Pulse.Syntax.Base.typ