Index of class methods


A
add [GuiList.pane]
add [GuiList.model]
add [ProverTask.command]
add_coqfile [ProverCoq.visitor]
add_dfile [ProverWhy3.visitor]
add_dfile [ProverErgo.visitor]
add_extlib [ProverWhy3.visitor]
add_float [ProverTask.command]
add_import [ProverWhy3.visitor]
add_import2 [ProverWhy3.visitor]
add_import3 [ProverWhy3.visitor]
add_int [ProverTask.command]
add_lemma [Generator.computer]
add_lemma [CfgWP.Computer.thecomputer]
add_lemma [CfgDump.computer]
add_library [ProverErgo.visitor]
add_list [ProverTask.command]
add_parameter [ProverTask.command]
add_positive [ProverTask.command]
add_rte [GuiSource.popup]
add_shared [ProverErgo.visitor]
add_strategy [Generator.computer]
add_strategy [CfgWP.Computer.thecomputer]
add_strategy [CfgDump.computer]
assume [Conditions.simplifier]

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

C
change_label [NormAtLabels.norm_at]
check [ProverCoq.runcoq]
clear [GuiNavigator.behavior]
clear [GuiSource.highlighter]
click [GuiGoal.prover]
coerce [GuiGoal.pane]
coerce [GuiList.pane]
coerce [GuiList.model]
coerce [GuiConfig.dp_button]
column_of_prover [GuiList.pane]
compile [ProverCoq.runcoq]
compute [Generator.computer]
compute [CfgWP.Computer.thecomputer]
compute [CfgDump.computer]
configure [GuiList.pane]
configure [GuiConfig.dp_chooser]
connect [GuiPanel.model_selector]
copy [Conditions.simplifier]
coqide [ProverCoq.runcoq]
count [Dyncall.dyncall]
count_selected [GuiList.pane]
create_prover [GuiList.pane]

D
datatype [Lang.idprinting]
datatypename [Lang.idprinting]
details [GuiNavigator.behavior]
detect [GuiConfig.dp_chooser]
detect [ProverWhy3.why3detect]
do_call [LogicUsage.visitor]
do_case [LogicUsage.visitor]
do_local [Definitions.visitor]
do_lvar [LogicUsage.visitor]
do_var [LogicUsage.visitor]

E
enable [GuiConfig.dp_chooser]
entry [GuiConfig.dp_chooser]
error [ProverWhy3.why3]
error [ProverErgo.altergo]

F
failed [ProverCoq.runcoq]
field [Lang.idprinting]
fieldname [Lang.idprinting]
fixpoint [Conditions.simplifier]
flush [ProverWhy3.visitor]
flush [ProverCoq.visitor]
flush [ProverErgo.visitor]
funname [Lang.idprinting]

G
get [GuiPanel.model_selector]
get [GuiList.pane]
get [GuiList.model]
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_after [ProverTask.group]
get_float [ProverTask.pattern]
get_float [ProverTask.group]
get_int [ProverTask.pattern]
get_int [ProverTask.group]
get_selection [GuiConfig.dp_button]
get_string [ProverTask.pattern]
get_string [ProverTask.group]
goal [GuiGoal.pane]

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

I
import [GuiConfig.dp_button]
index [GuiList.pane]
index [GuiList.model]
infer [Conditions.simplifier]
infoprover [Lang.idprinting]
Specify the field to use in an infoprover
iter_selected [GuiList.pane]

L
lemma [Generator.computer]
lemma [CfgWP.Computer.thecomputer]
lemma [CfgDump.computer]
limit [ProverWhy3.why3]
limit [ProverErgo.altergo]
lines [ProverTask.printer]
link [Lang.idprinting]
load [GuiConfig.provers]
log [GuiGoal.pane]
lookup [GuiConfig.dp_chooser]

M
move [GuiNavigator.behavior]

N
name [Conditions.simplifier]
navigator [GuiNavigator.behavior]
next [GuiNavigator.behavior]
next [ProverTask.group]

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

P
paragraph [ProverTask.printer]
popup [GuiNavigator.behavior]
popup_delete [GuiNavigator.behavior]
popup_proofmodes [GuiNavigator.behavior]
popup_run [GuiNavigator.behavior]
popup_why3ide [GuiNavigator.behavior]
prev [GuiNavigator.behavior]
printf [ProverTask.printer]
prove [GuiNavigator.behavior]
prove [ProverWhy3.why3]
prove [ProverErgo.altergo]
prover [ProverWhy3.why3detect]
prover_of_column [GuiList.pane]

R
register [GuiSource.popup]
reload [GuiNavigator.behavior]
reload [GuiList.pane]
reload [GuiList.model]
restore_pred [NormAtLabels.norm_at]
restore_term [NormAtLabels.norm_at]
result [ProverWhy3.why3detect]
result [ProverWhy3.why3]
result [ProverErgo.altergo]
rte_popup [GuiSource.popup]
run [GuiPanel.model_selector]
run [GuiGoal.pane]
run [GuiConfig.dp_chooser]
Edit enabled provers
run [ProverTask.command]

S
save [GuiConfig.provers]
scroll [GuiSource.highlighter]
search [ProverTask.group]
section [ProverTask.printer]
section [Definitions.visitor]
Comment
section [LogicUsage.visitor]
select [GuiGoal.pane]
select [GuiConfig.dp_chooser]
set [GuiPanel.model_selector]
set [GuiSource.highlighter]
set_command [ProverTask.command]
set_display [GuiGoal.prover]
set_enabled [GuiConfig.dp_button]
set_filter [GuiNavigator.behavior]
set_focus [GuiNavigator.behavior]
set_local [Definitions.visitor]
set_provers [GuiConfig.dp_button]
set_selection [GuiNavigator.behavior]
set_selection [GuiConfig.dp_button]
show [GuiList.pane]
simplify [Conditions.simplifier]
size [GuiList.pane]
size [GuiList.model]
start [ProverWhy3.why3ide]
stmt [Dyncall.dyncall]

T
target [Conditions.simplifier]
time [ProverWhy3.why3]
time [ProverErgo.altergo]
timeout [ProverTask.command]

U
unknown_prover [ProverWhy3.why3]
unsat [ProverErgo.altergo]
update [GuiNavigator.behavior]
update [GuiPanel.model_selector]
update [GuiSource.highlighter]
update [GuiGoal.pane]
update [GuiList.pane]
update [GuiConfig.dp_button]
update_all [GuiList.pane]

V
vadt [Definitions.visitor]
valid [ProverWhy3.why3]
valid [ProverErgo.altergo]
validate_pattern [ProverTask.command]
validate_time [ProverTask.command]
vannotation [Variables_analysis.logic_parameters_and_addr_taken_collection]
vannotation [LogicUsage.visitor]
vcluster [Definitions.visitor]
vcomp [Definitions.visitor]
vdefinition [Definitions.visitor]
vdfun [Definitions.visitor]
vdlemma [Definitions.visitor]
vexpr [Variables_analysis.parameters_call_kind_analysis]
vexpr [Variables_analysis.logic_parameters_and_addr_taken_collection]
vexpr [VarUsage.visitor]
vfield [Definitions.visitor]
vfunc [LogicUsage.visitor]
vfunc [Dyncall.dyncall]
vgoal [Definitions.visitor]
vinst [Variables_analysis.calls_collection]
vinst [Variables_analysis.parameters_call_kind_analysis]
vinst [VarUsage.visitor]
vinst [Dyncall.dyncall]
vlemma [Definitions.visitor]
vlfun [Definitions.visitor]
vlibrary [Definitions.visitor]
vlval [LogicUsage.visitor]
vparam [Definitions.visitor]
vpred [Definitions.visitor]
vpredicate [Variables_analysis.calls_collection]
vpredicate [Variables_analysis.parameters_call_kind_analysis]
vpredicate [Variables_analysis.logic_parameters_and_addr_taken_collection]
vpredicate [VarUsage.visitor]
vpredicate [LogicUsage.visitor]
vpredicate_named [NormAtLabels.norm_at]
vproperties [Definitions.visitor]
vself [Definitions.visitor]
vspec [VarUsage.visitor]
vspec [Dyncall.dyncall]
vsymbol [Definitions.visitor]
vtau [Definitions.visitor]
vterm [Definitions.visitor]
vterm [NormAtLabels.norm_at]
vterm [Variables_analysis.calls_collection]
vterm [Variables_analysis.parameters_call_kind_analysis]
vterm [Variables_analysis.logic_parameters_and_addr_taken_collection]
vterm [VarUsage.visitor]
vterm_lval [LogicUsage.visitor]
vterm_node [LogicUsage.visitor]
vtrigger [Definitions.visitor]
vtype [Definitions.visitor]
vtypedef [Definitions.visitor]

W
widget [GuiGoal.prover]
wp_popup [GuiSource.popup]