let inv_eloc_union (i, e, b) (i', e', b') = Inv_conj i i', Eloc_union e e', On_success_union b b'
let inv_eloc_union (i, e, b) (i', e', b') =
Inv_conj i i', Eloc_union e e', On_success_union b b'
InterpreterTarget.fst.checked
Target.fsti.checked prims.fst.checked Hashtable.fsti.checked FStar.String.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.All.fst.checked Ast.fst.checked
InterpreterTarget.fst
FStar.Pervasives.Native.tuple3 InterpreterTarget.inv InterpreterTarget.eloc InterpreterTarget.on_success FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.Mktuple3 InterpreterTarget.Inv_conj InterpreterTarget.Eloc_union InterpreterTarget.On_success_union
(*
   Copyright 2021 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module InterpreterTarget
(* The abstract syntax for the code produced by 3d, targeting prelude/Interpreter.fst *)
open FStar.All
open FStar.List.Tot
module A = Ast
module T = Target
module H = Hashtable

noeq
type inv =
  | Inv_true : inv
  | Inv_conj : inv -> inv -> inv
  | Inv_ptr  : A.ident -> inv
  | Inv_name : A.ident -> list expr -> inv

noeq
type eloc =
  | Eloc_none   : eloc
  | Eloc_output : eloc
  | Eloc_union  : eloc -> eloc -> eloc
  | Eloc_ptr    : A.ident -> eloc
  | Eloc_name   : A.ident -> list expr -> eloc

noeq
type on_success =
  | On_success : bool -> on_success
  | On_success_named : A.ident -> list expr -> on_success
  | On_success_union : on_success -> on_success -> on_success

let inv_eloc = inv & eloc & on_success
val inv_eloc_union : _: ((InterpreterTarget.inv * InterpreterTarget.eloc) * InterpreterTarget.on_success) ->
    _: ((InterpreterTarget.inv * InterpreterTarget.eloc) * InterpreterTarget.on_success)
  -> (InterpreterTarget.inv * InterpreterTarget.eloc) * InterpreterTarget.on_success

    _: ((InterpreterTarget.inv * InterpreterTarget.eloc) * InterpreterTarget.on_success) ->
    _: ((InterpreterTarget.inv * InterpreterTarget.eloc) * InterpreterTarget.on_success)
  -> (InterpreterTarget.inv * InterpreterTarget.eloc) * InterpreterTarget.on_success