Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
20 May 2022, 15:51:20 UTC
Revision f5d072e9a2cdd466d7587b09ced3d53bffde114d authored by Christian Doczkal on 19 October 2021, 17:49:56 UTC, committed by Pierre-Yves Strub on 04 November 2021, 10:00:49 UTC 
reduction from N to 1 oracle call for sdist distinguisher
1 parent 3adc9c8
Raw File
Tip revision: f5d072e9a2cdd466d7587b09ced3d53bffde114d authored by Christian Doczkal on 19 October 2021, 17:49:56 UTC
reduction from N to 1 oracle call for sdist distinguisher
Tip revision: f5d072e
ecCoreHiPhl.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 EcTypes
open EcModules
open EcFol
open EcLogic

(* -------------------------------------------------------------------- *)
val process_phl_form     : ty -> goal -> pformula -> form
val process_phl_formula  : goal -> pformula -> form
val process_phl_exp      : bool option -> pexpr -> ty option -> goal -> expr

val process_prhl_form    : ty -> goal -> pformula -> form
val process_prhl_formula : goal -> pformula -> form
val process_prhl_post    : goal -> pformula -> form

val process_prhl_stmt    : bool -> goal -> pstmt -> stmt
back to top