let preorder (c:C.const_buffer LP.byte) = C.qbuf_pre (C.as_qbuf c)
let preorder (c: C.const_buffer LP.byte) =
C.qbuf_pre (C.as_qbuf c)
LowParse.Repr.fsti.checked
prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.ConstBuffer.fsti.checked LowStar.Buffer.fst.checked LowParse.Spec.Base.fsti.checked LowParse.SLow.Base.fst.checked LowParse.Low.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Bytes.fsti.checked
LowParse.Repr.fsti
LowStar.ConstBuffer.const_buffer LowParse.Bytes.byte LowStar.ConstBuffer.qbuf_pre LowStar.ConstBuffer.as_qbuf FStar.Preorder.preorder FStar.Seq.Base.seq
(*
  Copyright 2015--2019 INRIA and Microsoft Corporation

  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.

  Authors: T. Ramananandro, A. Rastogi, N. Swamy, A. Fromherz
*)
module LowParse.Repr

module LP = LowParse.Low.Base
module LS = LowParse.SLow.Base
module B = LowStar.Buffer
module HS = FStar.HyperStack
module C = LowStar.ConstBuffer
module U32 = FStar.UInt32

open FStar.Integers
open FStar.HyperStack.ST

module ST = FStar.HyperStack.ST
module I = LowStar.ImmutableBuffer

(* Summary:

   A pointer-based representation type.

   See
   https://github.com/mitls/mitls-papers/wiki/The-Memory-Model-of-miTLS#pointer-based-transient-reprs

   Calling it LowParse.Ptr since it should eventually move to everparse/src/lowparse
 *)

/// `strong_parser_kind`: We restrict our attention to the
/// representation of types whose parsers have the strong-prefix
/// property.
let strong_parser_kind =
    k:LP.parser_kind{
      LP.(k.parser_kind_subkind == Some ParserStrong)
    }
val preorder : c: LowStar.ConstBuffer.const_buffer LowParse.Bytes.byte
  -> FStar.Preorder.preorder (FStar.Seq.Base.seq LowParse.Bytes.byte)
c: LowStar.ConstBuffer.const_buffer LowParse.Bytes.byte
  -> FStar.Preorder.preorder (FStar.Seq.Base.seq LowParse.Bytes.byte)