val parser_kind_prop (#a:Type) (k:parser_kind) (f:bare_parser a) : GTot Type0
let parser_kind_prop = parser_kind_prop'
val parser_kind_prop (#a:Type) (k:parser_kind) (f:bare_parser a) : GTot Type0
let parser_kind_prop =
parser_kind_prop'
LowParse.Spec.Base.fst.checked
prims.fst.checked LowParse.Bytes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Base.fst
LowParse.Spec.Base.parser_kind_prop'
module LowParse.Spec.Base
include LowParse.Bytes

module Seq = FStar.Seq
module U8 = FStar.UInt8
module U32 = FStar.UInt32
val parser_kind_prop (#a:Type) (k:parser_kind) (f:bare_parser a) : GTot Type0
k: LowParse.Spec.Base.parser_kind -> f: LowParse.Spec.Base.bare_parser a -> Prims.GTot Type0