Monadic.Delayed
val return :
?learned:Gillian.Gil_syntax.Formula.t list ->
?learned_types:(string * Gillian.Gil_syntax.Type.t) list ->
'a ->
'a t
val resolve_loc : Gillian.Gil_syntax.Expr.t -> string option t
val reduce : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t t
val reduce_formula :
Gillian.Gil_syntax.Formula.t ->
Gillian.Gil_syntax.Formula.t t
val entails :
Gillian.Gil_syntax.Formula.t list ->
Gillian.Gil_syntax.Formula.t ->
bool t
val check_sat : Gillian.Gil_syntax.Formula.t -> bool t
val vanish : unit -> 'a t
val if_sure :
Gillian.Gil_syntax.Formula.t ->
then_:(unit -> 'a t) ->
else_:(unit -> 'a t) ->
'a t
val branch_entailment :
(Gillian.Gil_syntax.Formula.t * (unit -> 'a t)) list ->
'a t
val leak_pc_copy : unit -> Engine.Gpc.t t
val branch_on :
Gillian.Gil_syntax.Formula.t ->
then_:(unit -> 'a t) ->
else_:(unit -> 'a t) ->
'a t
module Syntax : sig ... end