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

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

C
coerce [GuiGoal.pane]
coerce [GuiList.pane]
compute [Generator.computer]
copy [Conditions.simplifier]
count_selected [GuiList.pane]

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

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

G
get [GuiList.pane]
get [Toolbox.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.
infoprover [Lang.idprinting]
Specify the field to use in an infoprover
iter_selected [GuiList.pane]

L
lemma [Generator.computer]
lines [ProverTask.printer]
link [Lang.idprinting]

N
name [Conditions.simplifier]

O
on_click [GuiSource.popup]
on_click [GuiList.pane]
on_cluster [Definitions.visitor]
Outer cluster to import
on_comp [Definitions.visitor]
This local compinfo must be defined
on_dfun [Definitions.visitor]
This local function must be defined
on_dlemma [Definitions.visitor]
This local lemma must be defined
on_double_click [GuiList.pane]
on_library [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

P
paragraph [ProverTask.printer]
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
select [GuiGoal.pane]
send [Toolbox.selector]
set [GuiSource.highlighter]
set [Toolbox.selector]
set_command [ProverTask.command]
set_local [Definitions.visitor]
show [GuiList.pane]
simplify_branch [Conditions.simplifier]
Currently simplify a branch condition.
simplify_goal [Conditions.simplifier]
Simplify the goal.
simplify_hyp [Conditions.simplifier]
Currently simplify an hypothesis before assuming it.
size [GuiList.pane]

T
target [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]
validate_pattern [ProverTask.command]
validate_time [ProverTask.command]
vcluster [Definitions.visitor]
vcomp [Definitions.visitor]
vfield [Definitions.visitor]
vgoal [Definitions.visitor]
vlemma [Definitions.visitor]
vlibrary [Definitions.visitor]
vparam [Definitions.visitor]
vpred [Definitions.visitor]
vself [Definitions.visitor]
vsymbol [Definitions.visitor]
vtau [Definitions.visitor]
vterm [Definitions.visitor]
vtype [Definitions.visitor]