val normal (#a: Type) (x: a) : a
let normal (#a: Type) (x: a) : a =
  FStar.Pervasives.norm [
      iota;
      zeta;
      delta_only [`%L.fold_right_gtot; `%L.map_gtot];
      delta_attr [`%__reduce__];
      primops;
      simplify
    ]
    x
val normal (#a: Type) (x: a) : a
let normal (#a: Type) (x: a) : a =
FStar.Pervasives.norm [
    iota;
    zeta;
    delta_only [`%L.fold_right_gtot; `%L.map_gtot];
    delta_attr [`%__reduce__];
    primops;
    simplify
  ]
  x
FStar.BigOps.fsti.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
FStar.BigOps.fsti
FStar.Pervasives.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.iota FStar.Pervasives.zeta FStar.Pervasives.delta_only Prims.string Prims.Nil FStar.Pervasives.delta_attr FStar.Pervasives.primops FStar.Pervasives.simplify
(*
   Copyright 2008-2018 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.BigOps

/// This library provides propositional connectives over finite sets
/// expressed as lists, aka "big operators", in analogy with LaTeX
/// usage for \bigand, \bigor, etc.
///
/// The library is designed with a dual usage in mind:
///
///     1. Normalization: When applied to a list literal, we want
///        {[big_and f [a;b;c]]} to implicilty reduce to [f a /\ f b /\ f c]
///
///     2. Symbolic manipulation: We provide lemmas of the form
///
///        [big_and f l <==> forall x. L.memP x l ==> f x]
///
/// In this latter form, partially computing [big_and] as a fold over
/// a list is cumbersome for proof. So, we provide variants [big_and']
/// etc., that do not reduce implicitly.

module L = FStar.List.Tot

(** We control reduction using the [delta_attr] feature of the
    normalizer. See FStar.Pervasives for how that works. Every term
    that is to be reduced is with the [__reduce__] attribute *)
let __reduce__ = ()

(** We wrap [norm] with a module-specific custom usage, triggering
    specific reduction steps *)

[@@ __reduce__]
unfold
val normal (#a: Type) (x: a) : a
x: a -> a