sig
val array :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val choice :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val absurd :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val contrapose :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val compound :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val cut :
?priority:float ->
?modus:bool -> Wp.Tactical.selection -> Wp.Strategy.strategy
val filter : ?priority:float -> ?anti:bool -> unit -> Wp.Strategy.strategy
val havoc :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val separated :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val instance :
?priority:float ->
Wp.Tactical.selection ->
Wp.Tactical.selection list -> Wp.Strategy.strategy
val lemma :
?priority:float ->
?at:Wp.Tactical.selection ->
string -> Wp.Tactical.selection list -> Wp.Strategy.strategy
val intuition :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val range :
?priority:float ->
Wp.Tactical.selection -> vmin:int -> vmax:int -> Wp.Strategy.strategy
val split :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val definition :
?priority:float -> Wp.Tactical.selection -> Wp.Strategy.strategy
val auto_split : Wp.Strategy.heuristic
val auto_range : Wp.Strategy.heuristic
module Range :
sig
type rg
val compute : Wp.Conditions.sequence -> Wp.Auto.Range.rg
val ranges : Wp.Auto.Range.rg -> (int * int) Wp.Lang.F.Tmap.t
val bounds :
Wp.Auto.Range.rg -> (int option * int option) Wp.Lang.F.Tmap.t
end
val t_absurd : Wp.Tactical.process
val t_id : Wp.Tactical.process
val t_finally : string -> Wp.Tactical.process
val t_descr : string -> Wp.Tactical.process -> Wp.Tactical.process
val t_split :
?pos:string -> ?neg:string -> Wp.Lang.F.pred -> Wp.Tactical.process
val t_cut :
?by:string ->
Wp.Lang.F.pred -> Wp.Tactical.process -> Wp.Tactical.process
val t_case :
Wp.Lang.F.pred ->
Wp.Tactical.process -> Wp.Tactical.process -> Wp.Tactical.process
val t_cases :
?complete:string ->
(Wp.Lang.F.pred * Wp.Tactical.process) list -> Wp.Tactical.process
val t_chain :
Wp.Tactical.process -> Wp.Tactical.process -> Wp.Tactical.process
val t_range :
Wp.Lang.F.term ->
int ->
int ->
upper:Wp.Tactical.process ->
lower:Wp.Tactical.process ->
range:Wp.Tactical.process -> Wp.Tactical.process
val t_replace :
?equal:string ->
src:Wp.Lang.F.term ->
tgt:Wp.Lang.F.term -> Wp.Tactical.process -> Wp.Tactical.process
end