https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: 863066bded664a5e2aba7f89c4fb7bc2afd0e28d authored by Pierre-Yves Strub on 23 September 2015, 08:28:02 UTC
Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec`
Tip revision: 863066b
ecCoreHiPhl.mli
(* --------------------------------------------------------------------
 * Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
 * Distributed under the terms of the CeCILL-C 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