val and_then
  (#k: parser_kind)
  (#t:Type)
  (p:parser k t)
  (#k': parser_kind)
  (#t':Type)
  (p': (t -> Tot (parser k' t')))
: Pure (parser (and_then_kind k k') t')
  (requires (
    and_then_cases_injective p'
  ))
  (ensures (fun _ -> True))
let and_then #k #t p #k' #t' p' =
  let f : bare_parser t' = and_then_bare p p' in
  and_then_correct p p' ;
  f
val and_then
  (#k: parser_kind)
  (#t:Type)
  (p:parser k t)
  (#k': parser_kind)
  (#t':Type)
  (p': (t -> Tot (parser k' t')))
: Pure (parser (and_then_kind k k') t')
  (requires (
    and_then_cases_injective p'
  ))
  (ensures (fun _ -> True))
let and_then #k #t p #k' #t' p' =
let f:bare_parser t' = and_then_bare p p' in
and_then_correct p p';
f
LowParse.Spec.Combinators.fst.checked
prims.fst.checked LowParse.Spec.Base.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Combinators.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser Prims.unit LowParse.Spec.Combinators.and_then_correct LowParse.Spec.Base.bare_parser LowParse.Spec.Combinators.and_then_bare LowParse.Spec.Combinators.and_then_kind
module LowParse.Spec.Combinators
include LowParse.Spec.Base

module Seq = FStar.Seq
module U8 = FStar.UInt8
module U32 = FStar.UInt32

module T = FStar.Tactics

#reset-options "--using_facts_from '* -FStar.Tactis -FStar.Reflection'"
val and_then
  (#k: parser_kind)
  (#t:Type)
  (p:parser k t)
  (#k': parser_kind)
  (#t':Type)
  (p': (t -> Tot (parser k' t')))
: Pure (parser (and_then_kind k k') t')
  (requires (
    and_then_cases_injective p'
  ))
  (ensures (fun _ -> True))
p: LowParse.Spec.Base.parser k t -> p': (_: t -> LowParse.Spec.Base.parser k' t')
  -> Prims.Pure (LowParse.Spec.Base.parser (LowParse.Spec.Combinators.and_then_kind k k') t')