Wp.Strategy
Strategies Entry Points
val occurs_x : Lang.F.var -> Lang.F.term -> bool
val occurs_y : Lang.F.var -> Lang.F.pred -> bool
val occurs_e : Lang.F.term -> Lang.F.term -> bool
val occurs_p : Lang.F.term -> Lang.F.pred -> bool
val occurs_q : Lang.F.pred -> Lang.F.pred -> bool
val select_e : Conditions.sequent -> Lang.F.term -> Tactical.selection
Lookup the first occurrence of term in the sequent and returns the associated selection. Returns Empty
is not found. Goal is lookup first.
val select_p : Conditions.sequent -> Lang.F.pred -> Tactical.selection
Same as select_e
but for a predicate.
type strategy = {
priority : float; |
tactical : Tactical.tactical; |
selection : Tactical.selection; |
arguments : argument list; |
}
class pool : object ... end
class type heuristic = object ... end
val register : heuristic -> unit
val lookup : id:string -> heuristic
val iter : ( heuristic -> unit ) -> unit
type t = strategy
val arg : 'a Tactical.field -> 'a -> argument
val make :
Tactical.tactical ->
?priority:float ->
?arguments:argument list ->
Tactical.selection ->
strategy