Content - c5808c0ed69cc138e294f0d8514ea57731e4600f - 26c2b18/src/ecCoreHiPhl.mli

visit type:

https://github.com/EasyCrypt/easycrypt

05 April 2024, 19:20:55 UTC

Tip revision: 577c8820d4f34348e112814069730d16be6f970d authored by Pierre-Yves Strub on 27 April 2022, 09:41:00 UTC
Fix the license announced in the banner

Tip revision: 577c882

ecCoreHiPhl.mli

(* -------------------------------------------------------------------- *)
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