fact: Fixpoint Iterate_Equiv_QueryResultComp_body m {ResultT} (heading : RawHeading) (headings : Fin.t m -> RawHeading) (Ensembles : forall (idx : Fin.t m), @IndexedEnsemble (@RawTuple (headings idx))) (inj_Tuple : forall (idx : Fin.t m), @RawTuple (headings idx) -> @RawTuple heading) (body : @RawTuple heading -> Comp (list ResultT)) {struct m} : Comp (list ResultT) := match m return forall (headings : Fin.t m -> RawHeading), (forall (idx : Fin.t m), @IndexedEnsemble (@RawTuple (headings idx))) -> (forall (idx : Fin.t m), @RawTuple (headings idx) -> @RawTuple heading) -> Comp (list ResultT) with | 0 => fun _ _ _ => (ret List.nil) | S m => fun headings Ensembles inj_Tuple => res <- QueryResultComp (Ensembles Fin.F1) (fun tup => body (inj_Tuple Fin.F1 tup)); res' <- Iterate_Equiv_QueryResultComp_body heading (fun idx => headings (Fin.FS idx)) (fun idx => Ensembles (Fin.FS idx)) (fun idx tup => (inj_Tuple (Fin.FS idx) tup)) body ; ret (List.app res res') end headings Ensembles inj_Tuple.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.SumType Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Bedrock.Word Bedrock.Memory