fact: Definition rindexed_spec' P : ADT (string_rep Ascii.ascii String default_production_carrierT) := Def ADT { rep := T, Def Constructor1 "new" (s : String) : rep := ret s,, Def Method0 "to_string"(s : rep) : rep * String := ret (s, s), Def Method2 "char_at_matches"(s : rep) (n : nat) (P : Ascii.ascii -> bool) : rep * bool := ret (s, char_at_matches n s P), Def Method1 "get"(s : rep) (n : nat) : rep * Ascii.ascii := ret (s, unsafe_get n s), Def Method0 "length"(s : rep) : rep * nat := ret (s, length s), Def Method1 "take"(s : rep) (n : nat) : rep := ret (take n s), Def Method1 "drop"(s : rep) (n : nat) : rep := ret (drop n s), Def Method3 "splits"(s : rep) (idx : default_production_carrierT) (offset : nat) (len : nat) : rep * (list nat) := let dummy := nil in expanded_fallback_list' P s offset len idx dummy }.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.PeanoNat Coq.Lists.List Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ParserInterface Fiat.Parsers.ParserADTSpecification Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.Refinement.FixedLengthLemmas Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.Common Fiat.Common.Equality Fiat.Common.StringBound Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.Common.List.FlattenList Fiat.Common.List.ListMorphisms Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.StringFacts Fiat.Common.LogicFacts Fiat.Common.LogicMorphisms Fiat.Computation.SetoidMorphisms Fiat.Common.List.ListMorphisms Fiat.Common.Instances Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common Fiat.Common.Enumerable Fiat.Common.Enumerable.BoolProp Fiat.Common.Enumerable.ReflectiveForall Fiat.Common.Enumerable.ReflectiveForallStaged