val fold_left_dec (#a #b: _) (acc: a) (l: list b) (f: (a -> x: b{x << l} -> a))
    : Tot a (decreases l)
let rec fold_left_dec #a #b
  (acc : a)
  (l : list b)
  (f : a -> (x:b{x << l}) -> a)
  : Tot a (decreases l)
  =
  match l with
  | [] -> acc
  | x::xs -> fold_left_dec (f acc x) xs f
val fold_left_dec (#a #b: _) (acc: a) (l: list b) (f: (a -> x: b{x << l} -> a))
    : Tot a (decreases l)
let rec fold_left_dec #a #b (acc: a) (l: list b) (f: (a -> x: b{x << l} -> a)) : Tot a (decreases l) =
match l with
| [] -> acc
| x :: xs -> fold_left_dec (f acc x) xs f
FStar.Reflection.Typing.fsti.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Sealed.Inhabited.fst.checked FStar.Reflection.V2.Data.fsti.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
FStar.Reflection.Typing.fsti
Prims.list Prims.precedes FStar.Reflection.Typing.fold_left_dec
(*
   Copyright 2008-2023 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.
*)

module FStar.Reflection.Typing

(** This module defines a typing judgment for (parts of) the total
    and ghost fragment of F*.
    
    We are using it in the meta DSL framework as an
    official specification for the F* type system.

    We expect it to grow to cover more of the F* language.

    IT IS HIGHLY EXPERIMENTAL AND NOT YET READY TO USE.
  *)

open FStar.List.Tot
open FStar.Reflection.V2
module L = FStar.List.Tot
module R = FStar.Reflection.V2
module T = FStar.Tactics.V2
module RD = FStar.Reflection.V2.Data

(* MOVE to some helper module *)
let rec fold_left_dec #a #b
  (acc : a)
  (l : list b)
  (f : a -> (x:b{x << l}) -> a)
  : Tot a (decreases l)
val fold_left_dec (#a #b: _) (acc: a) (l: list b) (f: (a -> x: b{x << l} -> a))
    : Tot a (decreases l)
acc: a -> l: Prims.list b -> f: (_: a -> x: b{x << l} -> a) -> Prims.Tot a