val init_func_from_expr
      (#c: _)
      (#n0: int)
      (#nk: not_less_than n0)
      (expr: ((ifrom_ito n0 nk) -> c))
      (a: ifrom_ito n0 nk)
      (b: ifrom_ito a nk)
    : (counter_for (ifrom_ito a b) -> c)
let init_func_from_expr #c (#n0: int) (#nk: not_less_than n0) 
                        (expr: (ifrom_ito n0 nk) -> c) 
                        (a: ifrom_ito n0 nk) (b: ifrom_ito a nk) 
  : (counter_for (ifrom_ito a b) -> c)
  = fun (i: counter_for (ifrom_ito a b)) -> expr (n0 + i)
val init_func_from_expr
      (#c: _)
      (#n0: int)
      (#nk: not_less_than n0)
      (expr: ((ifrom_ito n0 nk) -> c))
      (a: ifrom_ito n0 nk)
      (b: ifrom_ito a nk)
    : (counter_for (ifrom_ito a b) -> c)
let init_func_from_expr
      #c
      (#n0: int)
      (#nk: not_less_than n0)
      (expr: ((ifrom_ito n0 nk) -> c))
      (a: ifrom_ito n0 nk)
      (b: ifrom_ito a nk)
    : (counter_for (ifrom_ito a b) -> c) =
fun (i: counter_for (ifrom_ito a b)) -> expr (n0 + i)
FStar.Algebra.CommMonoid.Fold.fsti.checked
prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.Permutation.fsti.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.IntegerIntervals.fst.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
FStar.Algebra.CommMonoid.Fold.fsti
Prims.int FStar.IntegerIntervals.not_less_than FStar.IntegerIntervals.ifrom_ito FStar.IntegerIntervals.counter_for Prims.op_Addition
(*
   Copyright 2008-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
*)

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

open FStar.Seq.Base
open FStar.Seq.Properties 
open FStar.Seq.Permutation

open FStar.IntegerIntervals
open FStar.Mul  


(* Here we define the notion for big sums and big products for 
   arbitrary commutative monoids. We construct the folds from 
   an integer range and a function, then calculate the fold --
   a sum or a product, depending on the monoid operation. *)
 
(* We refine multiplication a bit to make proofs smoothier *)


(* Notice how we can't just use a and b if we don't want to break 
   recursive calls with the same exprs *)
let init_func_from_expr #c (#n0: int) (#nk: not_less_than n0) 
                        (expr: (ifrom_ito n0 nk) -> c) 
                        (a: ifrom_ito n0 nk) (b: ifrom_ito a nk)
val init_func_from_expr
      (#c: _)
      (#n0: int)
      (#nk: not_less_than n0)
      (expr: ((ifrom_ito n0 nk) -> c))
      (a: ifrom_ito n0 nk)
      (b: ifrom_ito a nk)
    : (counter_for (ifrom_ito a b) -> c)

    expr: (_: FStar.IntegerIntervals.ifrom_ito n0 nk -> c) ->
    a: FStar.IntegerIntervals.ifrom_ito n0 nk ->
    b: FStar.IntegerIntervals.ifrom_ito a nk ->
    _: FStar.IntegerIntervals.counter_for (FStar.IntegerIntervals.ifrom_ito a b)
  -> c