https://github.com/EasyCrypt/easycrypt
Revision bb0a97ab2e0c8457087e6ccb1c9c160af5bc5a52 authored by Pierre-Yves Strub on 13 January 2021, 15:15:47 UTC, committed by Pierre-Yves Strub on 13 January 2021, 15:15:47 UTC
1 parent 88e05a0
Tip revision: bb0a97ab2e0c8457087e6ccb1c9c160af5bc5a52 authored by Pierre-Yves Strub on 13 January 2021, 15:15:47 UTC
Axiomatized operators are now forcibly unfoldable
Axiomatized operators are now forcibly unfoldable
Tip revision: bb0a97a
ecPhlRCond.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcParsetree
open EcCoreGoal.FApi
(* -------------------------------------------------------------------- *)
module Low : sig
val t_hoare_rcond : bool -> codepos1 -> backward
val t_bdhoare_rcond : bool -> codepos1 -> backward
val t_equiv_rcond : side -> bool -> codepos1 -> backward
end
(* -------------------------------------------------------------------- *)
val t_rcond : oside -> bool -> codepos1 -> backward
Computing file changes ...