Up
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
]