val valid
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: GTot Type0
let valid
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: GTot Type0
= valid' p h s pos
val valid
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: GTot Type0
let valid
      (#rrel #rel: _)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (s: slice rrel rel)
      (pos: U32.t)
    : GTot Type0 =
valid' p h s pos
LowParse.Low.Base.Spec.fst.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowParse.Math.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
LowParse.Low.Base.Spec.fst
LowParse.Slice.srel LowParse.Bytes.byte LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser FStar.Monotonic.HyperStack.mem LowParse.Slice.slice FStar.UInt32.t LowParse.Low.Base.Spec.valid'
module LowParse.Low.Base.Spec

module M = LowParse.Math
module B = LowStar.Monotonic.Buffer
module U32 = FStar.UInt32
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module Seq = FStar.Seq

let valid
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
val valid
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: GTot Type0

    p: LowParse.Spec.Base.parser k t ->
    h: FStar.Monotonic.HyperStack.mem ->
    s: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t
  -> Prims.GTot Type0