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