swh:1:snp:960b089228f647a5f611503985d0a438173f35bc
Tip revision: 69c9c2e226e29abd4e169d8439b83c6c0aa6aef6 authored by Benjamin Gregoire on 11 November 2022, 08:06:12 UTC
add few lemmas on dfun
add few lemmas on dfun
Tip revision: 69c9c2e
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