val primitive_box_matches_primitive_td (b: primitive_box_t) (td: primitive_td_t) : bool
val primitive_box_matches_primitive_td (b: primitive_box_t) (td: primitive_td_t) : bool
let primitive_box_matches_primitive_td (b: primitive_box_t) (td: primitive_td_t) : bool =
  primitive_box_to_td b = td
module Armada.Type

open Armada.Base
open Armada.BoundedInt
open Spec.Map
open Spec.Ubool
open FStar.Sequence.Base
open Util.Seq

/// "td" stands for "type descriptor"

type primitive_td_t =
  | PrimitiveTDBool: primitive_td_t
  | PrimitiveTDBoundedInt: (bt: bounded_int_type_t) -> primitive_td_t
  | PrimitiveTDThreadId: primitive_td_t
  | PrimitiveTDPointer: primitive_td_t

type primitive_box_t =
  | PrimitiveBoxBool: (b: bool) -> primitive_box_t
  | PrimitiveBoxBoundedInt: (bt: bounded_int_type_t) -> (n: bt_to_ty bt) -> primitive_box_t
  | PrimitiveBoxThreadId: (tid: tid_t) -> primitive_box_t
  | PrimitiveBoxPointer: (ptr: Armada.Pointer.t) -> primitive_box_t

let primitive_td_to_type (td: primitive_td_t) : Type =
  match td with
  | PrimitiveTDBool -> bool
  | PrimitiveTDBoundedInt bt -> bt_to_ty bt
  | PrimitiveTDThreadId -> tid_t
  | PrimitiveTDPointer -> Armada.Pointer.t

let primitive_box_to_td (b: primitive_box_t) : primitive_td_t =
  match b with
  | PrimitiveBoxBool _ -> PrimitiveTDBool
  | PrimitiveBoxBoundedInt bt _ -> PrimitiveTDBoundedInt bt
  | PrimitiveBoxThreadId _ -> PrimitiveTDThreadId
  | PrimitiveBoxPointer _ -> PrimitiveTDPointer

let primitive_box_to_type (b: primitive_box_t) : Type =
  primitive_td_to_type (primitive_box_to_td b)
/
Util.Seq.fsti.checked Spec.Ubool.fst.checked Spec.Map.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Sequence.Ambient.fst.checked FStar.Pervasives.fsti.checked Armada.Pointer.fst.checked Armada.BoundedInt.fst.checked Armada.Base.fst.checked
Armada.Type.fst
b: Armada.Type.primitive_box_t -> td: Armada.Type.primitive_td_t -> Prims.bool
Armada.Type.primitive_box_t Armada.Type.primitive_td_t Prims.op_Equality Armada.Type.primitive_box_to_td Prims.bool
let primitive_box_matches_primitive_td (b: primitive_box_t) (td: primitive_td_t) : bool =
  
primitive_box_to_td b = td