val transpose_generator
      (#c: _)
      (#m0 #mk #n0 #nk: int)
      (gen: (ifrom_ito m0 mk -> ifrom_ito n0 nk -> c))
    : (f: (ifrom_ito n0 nk -> ifrom_ito m0 mk -> c){forall i j. f j i == gen i j})
let transpose_generator #c (#m0 #mk: int)
                          (#n0 #nk: int)
                          (gen: ifrom_ito m0 mk -> ifrom_ito n0 nk -> c)
  : (f: (ifrom_ito n0 nk -> ifrom_ito m0 mk -> c) { forall i j. f j i == gen i j })
  = fun j i -> gen i j
val transpose_generator
      (#c: _)
      (#m0 #mk #n0 #nk: int)
      (gen: (ifrom_ito m0 mk -> ifrom_ito n0 nk -> c))
    : (f: (ifrom_ito n0 nk -> ifrom_ito m0 mk -> c){forall i j. f j i == gen i j})
let transpose_generator
      #c
      (#m0: int)
      (#mk: int)
      (#n0: int)
      (#nk: int)
      (gen: (ifrom_ito m0 mk -> ifrom_ito n0 nk -> c))
    : (f: (ifrom_ito n0 nk -> ifrom_ito m0 mk -> c){forall i j. f j i == gen i j}) =
fun j i -> gen i j
FStar.Algebra.CommMonoid.Fold.Nested.fsti.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.IntegerIntervals.fst.checked FStar.Algebra.CommMonoid.Fold.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
FStar.Algebra.CommMonoid.Fold.Nested.fsti
Prims.int FStar.IntegerIntervals.ifrom_ito Prims.l_Forall Prims.eq2
(*
   Copyright 2022 Microsoft Research
   
   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at
   
       http://www.apache.org/licenses/LICENSE-2.0
       
   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Author: A. Rozanov
*)

(*
   Here we reason about nested folds of functions over arbitrary 
   integer intervals. We call such functions generators.
*)
 
module FStar.Algebra.CommMonoid.Fold.Nested

module CF = FStar.Algebra.CommMonoid.Fold
module CE = FStar.Algebra.CommMonoid.Equiv

open FStar.IntegerIntervals 

(* This constructs a generator function that has its arguments in reverse 
   order. Useful when reasoning about nested folds, transposed matrices, etc. 
   
   Note how this utility is more general than transposed_matrix_gen 
   found in FStar.Seq.Matrix -- but for zero-based domains, latter is 
   more convenient. *)
let transpose_generator #c (#m0 #mk: int)
                          (#n0 #nk: int)
                          (gen: ifrom_ito m0 mk -> ifrom_ito n0 nk -> c)
val transpose_generator
      (#c: _)
      (#m0 #mk #n0 #nk: int)
      (gen: (ifrom_ito m0 mk -> ifrom_ito n0 nk -> c))
    : (f: (ifrom_ito n0 nk -> ifrom_ito m0 mk -> c){forall i j. f j i == gen i j})
gen: (_: FStar.IntegerIntervals.ifrom_ito m0 mk -> _: FStar.IntegerIntervals.ifrom_ito n0 nk -> c)
  -> f:
    (_: FStar.IntegerIntervals.ifrom_ito n0 nk -> _: FStar.IntegerIntervals.ifrom_ito m0 mk -> c)
      { forall (i: FStar.IntegerIntervals.ifrom_ito m0 mk)
          (j: FStar.IntegerIntervals.ifrom_ito n0 nk).
          f j i == gen i j }