module Trigger: sig .. end
sig
end
val of_term : Wp.Lang.F.term -> Wp.Definitions.trigger
Wp.Lang.F.term -> Wp.Definitions.trigger
val of_pred : Wp.Lang.F.pred -> Wp.Definitions.trigger
Wp.Lang.F.pred -> Wp.Definitions.trigger
val vars : Wp.Definitions.trigger -> Wp.Lang.F.Vars.t
Wp.Definitions.trigger -> Wp.Lang.F.Vars.t