val gaccessor_synth_inv
  (#k: parser_kind)
  (#t1: Type)
  (p1: parser k t1)
  (#t2: Type)
  (f: t1 -> GTot t2)
  (g: t2 -> GTot t1)
  (u: squash (synth_inverse f g /\ synth_injective f))
: Tot (gaccessor p1 (parse_synth p1 f) (clens_synth_inv g f))
let gaccessor_synth_inv
  (#k: parser_kind)
  (#t1: Type)
  (p1: parser k t1)
  (#t2: Type)
  (f: t1 -> GTot t2)
  (g: t2 -> GTot t1)
  (u: squash (synth_inverse f g /\ synth_injective f))
: Tot (gaccessor p1 (parse_synth p1 f) (clens_synth_inv g f))
= gaccessor_prop_equiv p1 (parse_synth p1 f) (clens_synth_inv g f) (gaccessor_synth_inv' p1 f g u);
  gaccessor_synth_inv' p1 f g u
val gaccessor_synth_inv
  (#k: parser_kind)
  (#t1: Type)
  (p1: parser k t1)
  (#t2: Type)
  (f: t1 -> GTot t2)
  (g: t2 -> GTot t1)
  (u: squash (synth_inverse f g /\ synth_injective f))
: Tot (gaccessor p1 (parse_synth p1 f) (clens_synth_inv g f))
let gaccessor_synth_inv
      (#k: parser_kind)
      (#t1: Type)
      (p1: parser k t1)
      (#t2: Type)
      (f: (t1 -> GTot t2))
      (g: (t2 -> GTot t1))
      (u: squash (synth_inverse f g /\ synth_injective f))
    : Tot (gaccessor p1 (parse_synth p1 f) (clens_synth_inv g f)) =
gaccessor_prop_equiv p1 (parse_synth p1 f) (clens_synth_inv g f) (gaccessor_synth_inv' p1 f g u);
gaccessor_synth_inv' p1 f g u
LowParse.Low.Combinators.fst.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Buffer.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Low.Base.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
LowParse.Low.Combinators.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser Prims.squash Prims.l_and LowParse.Spec.Combinators.synth_inverse LowParse.Spec.Combinators.synth_injective LowParse.Low.Combinators.gaccessor_synth_inv' Prims.unit LowParse.Low.Base.Spec.gaccessor_prop_equiv LowParse.Spec.Combinators.parse_synth LowParse.Low.Combinators.clens_synth_inv LowParse.Low.Base.Spec.gaccessor
module LowParse.Low.Combinators
include LowParse.Low.Base
include LowParse.Spec.Combinators

module B = LowStar.Monotonic.Buffer
module B0 = LowStar.Buffer
module U32 = FStar.UInt32
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module U64 = FStar.UInt64
module Cast = FStar.Int.Cast

#set-options "--z3rlimit 16"

let gaccessor_synth
  (#k: parser_kind)
  (#t1: Type)
  (p1: parser k t1)
  (#t2: Type)
  (f: t1 -> GTot t2)
  (g: t2 -> GTot t1)
  (u: squash (synth_inverse f g /\ synth_injective f))
: Tot (gaccessor (parse_synth p1 f) p1 (clens_synth g f))
= synth_injective_synth_inverse_synth_inverse_recip f g ();
  gaccessor_prop_equiv (parse_synth p1 f) p1 (clens_synth g f) (gaccessor_synth' p1 f g u);
  gaccessor_synth' p1 f g u

let gaccessor_synth_eq
  (#k: parser_kind)
  (#t1: Type)
  (p1: parser k t1)
  (#t2: Type)
  (f: t1 -> GTot t2)
  (g: t2 -> GTot t1)
  (u: unit { synth_inverse f g /\ synth_injective f } )
  (input: bytes)
: Lemma
  (gaccessor_synth p1 f g u input == gaccessor_synth' p1 f g u input)
= ()

let gaccessor_synth_inv
  (#k: parser_kind)
  (#t1: Type)
  (p1: parser k t1)
  (#t2: Type)
  (f: t1 -> GTot t2)
  (g: t2 -> GTot t1)
  (u: squash (synth_inverse f g /\ synth_injective f))
val gaccessor_synth_inv
  (#k: parser_kind)
  (#t1: Type)
  (p1: parser k t1)
  (#t2: Type)
  (f: t1 -> GTot t2)
  (g: t2 -> GTot t1)
  (u: squash (synth_inverse f g /\ synth_injective f))
: Tot (gaccessor p1 (parse_synth p1 f) (clens_synth_inv g f))

    p1: LowParse.Spec.Base.parser k t1 ->
    f: (_: t1 -> Prims.GTot t2) ->
    g: (_: t2 -> Prims.GTot t1) ->
    u247:
      Prims.squash (LowParse.Spec.Combinators.synth_inverse f g /\
          LowParse.Spec.Combinators.synth_injective f)
  -> LowParse.Low.Base.Spec.gaccessor p1
      (LowParse.Spec.Combinators.parse_synth p1 f)
      (LowParse.Low.Combinators.clens_synth_inv g f)