Index of class methods


A
add [GuiList.pane]
add [ProverTask.command]
add_float [ProverTask.command]
add_int [ProverTask.command]
add_lemma [Generator.computer]
add_list [ProverTask.command]
add_parameter [ProverTask.command]
add_positive [ProverTask.command]
add_strategy [Generator.computer]
assume [Conditions.simplifier]
Assumes the hypothesis
assume [Wp.Conditions.simplifier]
Assumes the hypothesis

B
basename [Lang.idprinting]
Allows to sanitize the basename used for generated or ACSL name (not the one provided by the driver.
basename [Wp.Lang.idprinting]
Allows to sanitize the basename used for generated or ACSL name (not the one provided by the driver.

C
callstyle [Vlist.engine]
coerce [GuiGoal.pane]
coerce [GuiList.pane]
compute [Generator.computer]
copy [Conditions.simplifier]
copy [Wp.Conditions.simplifier]
count_selected [GuiList.pane]

D
datatype [Lang.idprinting]
datatype [Wp.Lang.idprinting]
datatypename [Lang.idprinting]
datatypename [Wp.Lang.idprinting]
do_local [Definitions.visitor]
do_local [Wp.Definitions.visitor]

F
field [Lang.idprinting]
field [Wp.Lang.idprinting]
fieldname [Lang.idprinting]
fieldname [Wp.Lang.idprinting]
fixpoint [Conditions.simplifier]
Called after assuming hypothesis and knowing the goal
fixpoint [Wp.Conditions.simplifier]
Called after assuming hypothesis and knowing the goal
funname [Lang.idprinting]
funname [Wp.Lang.idprinting]

G
get [GuiList.pane]
get [Widget.selector]
get_after [ProverTask.pattern]
get_after ~offset:p k returns the end of the message starting p characters after the end of group k.
get_float [ProverTask.pattern]
get_int [ProverTask.pattern]
get_string [ProverTask.pattern]

H
highlight [GuiSource.highlighter]
hline [ProverTask.printer]

I
index [GuiList.pane]
infer [Conditions.simplifier]
Add new hypotheses implyed by the original hypothesis.
infer [Wp.Conditions.simplifier]
Add new hypotheses implyed by the original hypothesis.
infoprover [Lang.idprinting]
Specify the field to use in an infoprover
infoprover [Wp.Lang.idprinting]
Specify the field to use in an infoprover
iter_selected [GuiList.pane]

L
lemma [Generator.computer]
lines [ProverTask.printer]
link [Lang.idprinting]
link [Wp.Lang.idprinting]
lookup [Plang.engine]

M
mark [Pcond.engine]
Marks terms to share in step
marks [Plang.engine]

N
name [Pcond.engine]
Printer Components
name [Conditions.simplifier]
name [Wp.Conditions.simplifier]

O
on_click [GuiSource.popup]
on_click [GuiList.pane]
on_cluster [Definitions.visitor]
Outer cluster to import
on_cluster [Wp.Definitions.visitor]
Outer cluster to import
on_comp [Definitions.visitor]
This local compinfo must be defined
on_comp [Wp.Definitions.visitor]
This local compinfo must be defined
on_dfun [Definitions.visitor]
This local function must be defined
on_dfun [Wp.Definitions.visitor]
This local function must be defined
on_dlemma [Definitions.visitor]
This local lemma must be defined
on_dlemma [Wp.Definitions.visitor]
This local lemma must be defined
on_double_click [GuiList.pane]
on_library [Definitions.visitor]
External library to import
on_library [Wp.Definitions.visitor]
External library to import
on_prove [GuiSource.popup]
on_right_click [GuiList.pane]
on_run [GuiGoal.pane]
on_selection [GuiList.pane]
on_src [GuiGoal.pane]
on_type [Definitions.visitor]
This local type must be defined
on_type [Wp.Definitions.visitor]
This local type must be defined

P
paragraph [ProverTask.printer]
pp_atom [Vlist.engine]
pp_clause [Pcond.engine]
Default: "@{<wp:clause>...}"
pp_comment [Pcond.engine]
Default: "@{<wp:comment>(* ... *)}"
pp_condition [Pcond.engine]
pp_core [Pcond.engine]
Default: plang#pp_sort
pp_definition [Pcond.engine]
pp_esequent [Pcond.engine]
Print the sequent in the given environment.
pp_flow [Vlist.engine]
pp_intro [Pcond.engine]
pp_name [Pcond.engine]
Default: Format.pp_print_string
pp_pred [Plang.engine]
pp_property [Pcond.engine]
Default: "@{<wp:property>(* ... *)}"
pp_sequence [Pcond.engine]
Assumes an "<hv>" box is opened.
pp_sequent [Pcond.engine]
Print the sequent in global environment.
pp_step [Pcond.engine]
Assumes an "<hv>" box is opened.
pp_warning [Pcond.engine]
Default: "@{<wp:warning>Warning}..."
printf [ProverTask.printer]

R
register [GuiSource.popup]
reload [GuiList.pane]
run [GuiConfig.dp_chooser]
Edit enabled provers
run [ProverTask.command]

S
section [ProverTask.printer]
section [Definitions.visitor]
Comment
section [Wp.Definitions.visitor]
Comment
select [GuiGoal.pane]
send [Widget.selector]
set [GuiSource.highlighter]
set [Widget.selector]
set_command [ProverTask.command]
set_local [Definitions.visitor]
set_local [Wp.Definitions.visitor]
show [GuiList.pane]
simplify_branch [Conditions.simplifier]
Currently simplify a branch condition.
simplify_branch [Wp.Conditions.simplifier]
Currently simplify a branch condition.
simplify_goal [Conditions.simplifier]
Simplify the goal.
simplify_goal [Wp.Conditions.simplifier]
Simplify the goal.
simplify_hyp [Conditions.simplifier]
Currently simplify an hypothesis before assuming it.
simplify_hyp [Wp.Conditions.simplifier]
Currently simplify an hypothesis before assuming it.
size [GuiList.pane]

T
target [Conditions.simplifier]
Give the predicate that will be simplified later
target [Wp.Conditions.simplifier]
Give the predicate that will be simplified later
timeout [ProverTask.command]

U
update [GuiSource.highlighter]
update [GuiGoal.pane]
update [GuiList.pane]
update [GuiConfig.dp_button]
update_all [GuiList.pane]

V
vadt [Definitions.visitor]
vadt [Wp.Definitions.visitor]
validate_pattern [ProverTask.command]
validate_time [ProverTask.command]
vcluster [Definitions.visitor]
vcluster [Wp.Definitions.visitor]
vcomp [Definitions.visitor]
vcomp [Wp.Definitions.visitor]
vfield [Definitions.visitor]
vfield [Wp.Definitions.visitor]
vgoal [Definitions.visitor]
vgoal [Wp.Definitions.visitor]
vlemma [Definitions.visitor]
vlemma [Wp.Definitions.visitor]
vlibrary [Definitions.visitor]
vlibrary [Wp.Definitions.visitor]
vparam [Definitions.visitor]
vparam [Wp.Definitions.visitor]
vpred [Definitions.visitor]
vpred [Wp.Definitions.visitor]
vself [Definitions.visitor]
vself [Wp.Definitions.visitor]
vsymbol [Definitions.visitor]
vsymbol [Wp.Definitions.visitor]
vtau [Definitions.visitor]
vtau [Wp.Definitions.visitor]
vterm [Definitions.visitor]
vterm [Wp.Definitions.visitor]
vtype [Definitions.visitor]
vtype [Wp.Definitions.visitor]