swh:1:snp:960b089228f647a5f611503985d0a438173f35bc
Tip revision: 5a7aca4d68a0fdd4521c2ae8c6604e277ef5a9d8 authored by Pierre Boutry on 10 November 2022, 18:08:49 UTC
add some examples
add some examples
Tip revision: 5a7aca4
ecPhlRCond.mli
(* -------------------------------------------------------------------- *)
open EcSymbols
open EcParsetree
open EcCoreGoal.FApi
(* -------------------------------------------------------------------- *)
module Low : sig
val t_hoare_rcond : bool -> codepos1 -> backward
val t_choare_rcond : bool -> codepos1 -> EcFol.form option -> backward
val t_bdhoare_rcond : bool -> codepos1 -> backward
val t_equiv_rcond : side -> bool -> codepos1 -> backward
end
(* -------------------------------------------------------------------- *)
module LowMatch : sig
val t_hoare_rcond_match : symbol -> codepos1 -> backward
val t_bdhoare_rcond_match : symbol -> codepos1 -> backward
val t_equiv_rcond_match : side -> symbol -> codepos1 -> backward
end
(* -------------------------------------------------------------------- *)
val t_rcond : oside -> bool -> codepos1 -> EcFol.form option -> backward
val process_rcond : oside -> bool -> codepos1 -> pformula option -> backward
val t_rcond_match : oside -> symbol -> codepos1 -> backward