Content - c5808c0ed69cc138e294f0d8514ea57731e4600f - 9d48bb4/src/ecCoreHiPhl.mli

visit type:

https://github.com/EasyCrypt/easycrypt

05 April 2024, 19:20:55 UTC

Tip revision: 3cef12a5d08bbaf7b486bd02ca6c194f4f167bea authored by Manuel Barbosa on 10 October 2023, 09:38:20 UTC
Making this branch work with same Why3 version as main

Tip revision: 3cef12a

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