let lmbuffer a r s l =
    b:LB.mbuffer a r s{
      LB.len b == l
    }
let lmbuffer a r s l =
b: LB.mbuffer a r s {LB.len b == l}
LowStar.Printf.fst.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.String.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Int8.fsti.checked FStar.Int64.fsti.checked FStar.Int32.fsti.checked FStar.Int16.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.Char.fsti.checked FStar.BigOps.fsti.checked
LowStar.Printf.fst
LowStar.Monotonic.Buffer.srel FStar.UInt32.t LowStar.Monotonic.Buffer.mbuffer Prims.eq2 LowStar.Monotonic.Buffer.len
(*
   Copyright 2008-2018 Microsoft Research

   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.
*)
module LowStar.Printf

/// This module provides imperative printing functions for several
/// primitive Low* types, including
///  -- booleans (%b)
///  -- characters (%c)
///  -- strings (%s)
///  -- machine integers
///          (UInt8.t as %uy, UInt16.t as %us, UInt32.t as %ul, and UInt64.t as %uL;
///            Int8.t  as %y,  Int16.t as %i,   Int32.t as %l , and  Int64.t as %L)
///  -- and arrays (aka buffers) of these base types formatted
///         as %xN, where N is the format specifier for the array element type
///         e.g., %xuy for buffers of UInt8.t

/// The main function of this module is `printf`
/// There are a few main differences relative to C printf
///   -- The format specifiers are different (see above)
///
///   -- For technical reasons explained below, an extra dummy
///      argument `done` has to be provided at the end for the
///      computation to have any effect.
///
///      E.g., one must write
///           `printf "%b %c" true 'c' done`
///      rather than just
///           `printf "%b %c" true 'c'`
///
///   -- When printing arrays, two arguments must be passed; the
///      length of the array fragment to be formatted and the array
///      itself
///
///   -- When extracted, rather than producing a C `printf` (which
///      does not, e.g., support printing of dynamically sized
///      arrays), our `printf` is specialized to a sequence of calls
///      to primitive printers for each supported type
///
/// Before diving into the technical details of how this module works,
/// you might want to see a sample usage at the very end of this file.

open FStar.Char
open FStar.String
open FStar.HyperStack.ST
module L = FStar.List.Tot
module LB = LowStar.Monotonic.Buffer

/// `lmbuffer a r s l` is
///    - a monotonic buffer of `a`
///    - governed by preorders `r` and `s`
///    - with length `l`
val lmbuffer : a: Type0 ->
    r: LowStar.Monotonic.Buffer.srel a ->
    s: LowStar.Monotonic.Buffer.srel a ->
    l: FStar.UInt32.t
  -> Type0

    a: Type0 ->
    r: LowStar.Monotonic.Buffer.srel a ->
    s: LowStar.Monotonic.Buffer.srel a ->
    l: FStar.UInt32.t
  -> Type0