fact: Definition StatefulInsertAll {qsSchema A S QS} (r : QS qsSchema) (idx : BoundedIndex (QSschemaNames qsSchema)) (st : S) (As : list A) (insertComp : QSInsertType qsSchema QS) (rowFunc : A -> S -> Comp (_ * S)) (failure : A -> S -> Comp S) : Comp (QS qsSchema * S) := foldComp (fun (acc : QS _ * S) a => let (r, st) := acc in p <- rowFunc a st; let (newRow, st') := p in res <- insertComp r (ibound (indexb idx)) newRow; let (r, b) := res in st'' <- If b Then ret st' Else failure a st'; ret (r, st'')) (r, st) As.
imports: Coq.Lists.List Coq.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.Common.StringBound Fiat.Common.Ensembles.IndexedEnsembles Fiat.Computation.FoldComp Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure