val base_typ_as_type (t: base_typ) : eqtype
let base_typ_as_type (t:base_typ) : eqtype =
  let open W in
  let open Vale.Def.Types_s in
  match t with
  | TUInt8 -> UInt8.t
  | TUInt16 -> UInt16.t
  | TUInt32 -> UInt32.t
  | TUInt64 -> UInt64.t
  | TUInt128 -> quad32
val base_typ_as_type (t: base_typ) : eqtype
let base_typ_as_type (t: base_typ) : eqtype =
let open W in
let open Vale.Def.Types_s in
match t with
| TUInt8 -> UInt8.t
| TUInt16 -> UInt16.t
| TUInt32 -> UInt32.t
| TUInt64 -> UInt64.t
| TUInt128 -> quad32
Vale.Interop.Types.fst.checked
Vale.Interop.Views.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Vale.Interop.Types.fst
Vale.Arch.HeapTypes_s.base_typ FStar.UInt8.t FStar.UInt16.t FStar.UInt32.t FStar.UInt64.t Vale.Def.Types_s.quad32 Prims.eqtype
module Vale.Interop.Types
open FStar.Mul
include Vale.Arch.HeapTypes_s
module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module MB = LowStar.Monotonic.Buffer
module DV = LowStar.BufferView.Down
module W = Vale.Def.Words_s
module L = FStar.List.Tot

[@__reduce__]
val base_typ_as_type (t: base_typ) : eqtype
t: Vale.Arch.HeapTypes_s.base_typ -> Prims.eqtype