fact: Definition string_spec' : ADT (string_rep Ascii.ascii String default_production_carrierT) := Def ADT { rep := String, 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 := b <- { b : bool | forall ch', get n s = Some ch' -> P ch' = b }; ret (s, b), Def Method1 "get"(s : rep) (n : nat) : rep * Ascii.ascii := ch <- { ch : Ascii.ascii | forall ch', get n s = Some ch' -> ch = ch' }; ret (s, ch), 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 := ls <- { ls : list nat | split_list_is_complete_idx G s offset len idx ls }; ret (s, ls) }.
imports: Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.Parsers.ParserInterface Fiat.Parsers.ContextFreeGrammar.PreNotations