val implies_elim: p: Type -> q: Type -> squash (p ==> q) -> f: (unit -> Tot (squash p)) -> squash q
let implies_elim
        (p:Type)
        (q:Type)
        (_:squash (p ==> q))
        (f:unit -> Tot (squash p))
  : squash q
  = f()
val implies_elim: p: Type -> q: Type -> squash (p ==> q) -> f: (unit -> Tot (squash p)) -> squash q
let implies_elim (p: Type) (q: Type) (_: squash (p ==> q)) (f: (unit -> Tot (squash p))) : squash q =
f ()
FStar.Classical.Sugar.fsti.checked
prims.fst.checked FStar.Pervasives.fsti.checked
FStar.Classical.Sugar.fsti
Prims.squash Prims.l_imp Prims.unit
(*
   Copyright 2021 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.Classical.Sugar

/// This module provides a few combinators that are targeted
/// by the desugaring phase of the F* front end
///
/// The combinators it provides are fairly standard, except for one
/// subtlety. In F*, the typechecking of terms formed using the
/// logical connectives is biased from left to right. That is:
///
/// * In [p /\ q] and [p ==> q], the well-typedness of [q] is in a
///   context assuming [squash p]
///
/// * In [p \/ q], the well-typedness of [q] is in a context assuming
///   [squash (~p)]
///
/// So, many of these combinators reflect that bias by taking as
/// instantiations for [q] functions that depend on [squash p] or
/// [squash (~p)].
///
/// The other subtlety is that the when using these combinators, we
/// encapsulate any proof terms provided by the caller within a
/// thunk. This is to ensure that if, for instance, the caller simply
/// admits a goal, that they do not inadvertently discard any proof
/// obligations in the remainder of their programs.
///
/// For example, consider the difference between
///
///  1. exists_intro a p v (admit()); rest
///
/// and
///
///  2. exists_intro a p v (fun _ -> admit()); rest
///
/// In (1) the proof of rest is admitted also.


(** Eliminate a universal quantifier by providing an instantiation *)
val forall_elim
       (#a:Type)
       (#p:a -> Type)
       (v:a)
       (f:squash (forall (x:a). p x))
  : Tot (squash (p v))

(** Eliminate an existential quantifier into a proof of a goal [q] *)
val exists_elim
     (#t:Type)
     (#p:t -> Type)
     (#q:Type)
     ($s_ex_p: squash (exists (x:t). p x))
     (f: (x:t -> squash (p x) -> Tot (squash q)))
  : Tot (squash q)

(** Eliminate an implication, by providing a proof of the hypothesis
    Note, the proof is thunked *)
let implies_elim
        (p:Type)
        (q:Type)
        (_:squash (p ==> q))
        (f:unit -> Tot (squash p))
val implies_elim: p: Type -> q: Type -> squash (p ==> q) -> f: (unit -> Tot (squash p)) -> squash q
p: Type0 -> q: Type0 -> _: Prims.squash (p ==> q) -> f: (_: Prims.unit -> Prims.squash p)
  -> Prims.squash q