val elim_pure_wp_monotonicity (#a: Type) (wp: pure_wp a) : Lemma (is_monotonic wp)
let elim_pure_wp_monotonicity (#a:Type) (wp:pure_wp a)
  : Lemma (is_monotonic wp)
  = reveal_opaque (`%pure_wp_monotonic) pure_wp_monotonic
val elim_pure_wp_monotonicity (#a: Type) (wp: pure_wp a) : Lemma (is_monotonic wp)
let elim_pure_wp_monotonicity (#a: Type) (wp: pure_wp a) : Lemma (is_monotonic wp) =
reveal_opaque (`%pure_wp_monotonic) pure_wp_monotonic
FStar.Monotonic.Pure.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked
FStar.Monotonic.Pure.fst
Prims.pure_wp FStar.Pervasives.reveal_opaque Prims.pure_wp' Prims.logical Prims.pure_wp_monotonic Prims.unit Prims.l_True Prims.squash FStar.Monotonic.Pure.is_monotonic Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2019 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.Monotonic.Pure

(*
 * This module provides utilities to intro and elim the monotonicity
 *   property of pure wps
 *
 * Since pure_wp_monotonic predicate is marked opaque_to_smt in prims,
 *   reasoning with it requires explicit coercions
 *)

unfold
let is_monotonic (#a:Type) (wp:pure_wp' a) =
  (*
   * Once we support using tactics in ulib/,
   *   this would be written as: Prims.pure_wp_monotonic0,
   *   with a postprocessing tactic to norm it
   *)
  forall (p q:pure_post a). (forall (x:a). p x ==> q x) ==> (wp p ==> wp q)  

let elim_pure_wp_monotonicity (#a:Type) (wp:pure_wp a)
val elim_pure_wp_monotonicity (#a: Type) (wp: pure_wp a) : Lemma (is_monotonic wp)
wp: Prims.pure_wp a -> FStar.Pervasives.Lemma (ensures FStar.Monotonic.Pure.is_monotonic wp)