Index of class methods


A
add [GuiList.pane]
add [ProverTask.command]
add [Strategy.pool]
add [Wp.Strategy.pool]
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]
arity [Tactical.composer]
arity [Wp.Tactical.composer]
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.
button [GuiSequent.focused]

C
callstyle [Vlist.engine]
choose [GuiTactic.browser]
clear [GuiComposer.browser]
clear [GuiComposer.composer]
clear [GuiTactic.tactic]
clear [GuiProver.prover]
clear [Pcond.state]
coerce [GuiGoal.pane]
coerce [GuiList.pane]
command [ProverTask.command]
compute [Generator.computer]
compute [Tactical.composer]
compute [Wp.Tactical.composer]
connect [GuiComposer.browser]
request-for-update event
connect [GuiComposer.composer]
request-for-update event
connect [GuiTactic.strategies]
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]
descr [GuiTactic.browser]
descr [GuiTactic.composer]
descr [Strategy.heuristic]
descr [Tactical.composer]
descr [Tactical.tactical]
descr [Tactical.make]
descr [Wp.Strategy.heuristic]
descr [Wp.Tactical.composer]
descr [Wp.Tactical.tactical]
descr [Wp.Tactical.make]
do_local [Definitions.visitor]
do_local [Wp.Definitions.visitor]
domain [Pcond.state]

F
field [Lang.idprinting]
field [Wp.Lang.idprinting]
fieldname [Lang.idprinting]
fieldname [Wp.Lang.idprinting]
filter [Tactical.composer]
filter [Wp.Tactical.composer]
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_field [Tactical.tactical]
get_field [Tactical.make]
get_field [Wp.Tactical.tactical]
get_field [Wp.Tactical.make]
get_float [ProverTask.pattern]
get_focus_mode [GuiSequent.focused]
get_int [ProverTask.pattern]
get_state [Pcond.sequence]
If true, states are rendered when printing sequences.
get_state_mode [GuiSequent.focused]
get_string [ProverTask.pattern]
get_title [Tactical.feedback]
Retrieve the title
get_title [Wp.Tactical.feedback]
Retrieve the title
get_value [GuiTactic.composer]
goal [GuiSequent.focused]
group [Tactical.composer]
group [Wp.Tactical.composer]

H
has_error [Tactical.feedback]
Retrieve the errors
has_error [Wp.Tactical.feedback]
Retrieve the errors
highlight [GuiSource.highlighter]
hline [ProverTask.printer]

I
id [Strategy.heuristic]
id [Tactical.composer]
id [Tactical.tactical]
id [Tactical.make]
id [Wp.Strategy.heuristic]
id [Wp.Tactical.composer]
id [Wp.Tactical.tactical]
id [Wp.Tactical.make]
index [GuiList.pane]
infer [Conditions.simplifier]
Add new hypotheses implied by the original hypothesis.
infer [Wp.Conditions.simplifier]
Add new hypotheses implied 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
interactive [Tactical.feedback]
Interactive mode.
interactive [Wp.Tactical.feedback]
Interactive mode.
is_atomic_lv [Pcfg.engine]
is_valid [GuiTactic.composer]
iter_selected [GuiList.pane]

L
label_at [Pcond.state]
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]
model [Generator.computer]

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

O
on_backtrack [GuiProof.printer]
on_click [GuiSource.popup]
on_click [GuiProof.printer]
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_popup [GuiSequent.focused]
on_prove [GuiSource.popup]
on_right_click [GuiList.pane]
on_selection [GuiSequent.focused]
on_selection [GuiList.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]
params [Tactical.tactical]
params [Tactical.make]
params [Wp.Tactical.tactical]
params [Wp.Tactical.make]
pending [GuiProof.printer]
popup [GuiSequent.focused]
pp_addr [Pcfg.engine]
pp_at [Pcond.state]
pp_atom [Pcfg.engine]
pp_atom [Vlist.engine]
pp_block [Pcond.engine]
pp_chunk [Pcfg.engine]
chunk name
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 [Pcfg.engine]
pp_flow [Vlist.engine]
pp_goal [Pcond.engine]
pp_host [Pcfg.engine]
current state
pp_intro [Pcond.engine]
pp_label [Pcfg.engine]
label name
pp_lval [Pcfg.engine]
current state
pp_main [GuiProof.printer]
pp_name [Pcond.engine]
Default: Format.pp_print_string
pp_node [GuiProof.printer]
pp_offset [Pcfg.engine]
pp_ofs [Pcfg.engine]
pp_pred [GuiSequent.focused]
pp_pred [Plang.engine]
pp_property [Pcond.engine]
Default: "@{<wp:property>(* ... *)}"
pp_selection [GuiSequent.focused]
pp_sequence [Pcond.engine]
Assumes an "<hv>" box is opened and all variables are declared.
pp_sequent [GuiSequent.focused]
pp_sequent [Pcond.engine]
Print the sequent in global environment.
pp_step [Pcond.engine]
Assumes an "<hv>" box is opened.
pp_stmt [Pcond.engine]
Default: "@{<wp:stmt>...}"
pp_term [GuiSequent.focused]
pp_update [Pcond.state]
pp_value [Pcond.state]
pp_warning [Pcond.engine]
Default: "@{<wp:warning>Warning}..."
pretty [ProverTask.command]
print [GuiComposer.browser]
print [GuiComposer.composer]
printf [ProverTask.printer]
prover [GuiProver.prover]

R
ranged [GuiTactic.composer]
register [GuiSource.popup]
register [GuiTactic.strategies]
reload [GuiList.pane]
reset [GuiSequent.focused]
reset [Tactical.tactical]
reset [Tactical.make]
reset [Wp.Tactical.tactical]
reset [Wp.Tactical.make]
restore [GuiSequent.focused]
run [GuiConfig.dp_chooser]
Edit enabled provers
run [ProverTask.command]

S
search [GuiTactic.browser]
search [Strategy.heuristic]
search [Wp.Strategy.heuristic]
section [ProverTask.printer]
section [Definitions.visitor]
Comment
section [Wp.Definitions.visitor]
Comment
select [GuiGoal.pane]
select [GuiTactic.tactic]
select [Tactical.tactical]
select [Tactical.make]
Shall return Applicable or Not_configured if the tactic might apply to the selection.
select [Wp.Tactical.tactical]
select [Wp.Tactical.make]
Shall return Applicable or Not_configured if the tactic might apply to the selection.
selected [GuiSequent.focused]
selection [GuiSequent.focused]
send [Widget.selector]
sequent [GuiSequent.focused]
set [GuiSource.highlighter]
set [Widget.selector]
set_command [ProverTask.command]
set_descr [Tactical.feedback]
Add a short description wrt current selection & tuning
set_descr [Wp.Tactical.feedback]
Add a short description wrt current selection & tuning
set_domain [Pcond.state]
Default is sequence's domain
set_error [Tactical.feedback]
Mark the current configuration as invalid
set_error [Wp.Tactical.feedback]
Mark the current configuration as invalid
set_field [Tactical.tactical]
set_field [Tactical.make]
set_field [Wp.Tactical.tactical]
set_field [Wp.Tactical.make]
set_focus_mode [GuiSequent.focused]
set_goal [Pcond.sequence]
Adds goal to state domain
set_local [Definitions.visitor]
set_local [Wp.Definitions.visitor]
set_sequence [Pcond.sequence]
Initialize state with this sequence
set_sequence [Pcond.state]
set_sequent [Pcond.sequence]
Set sequence and goal
set_state [Pcond.sequence]
If set to false, states rendering is deactivated.
set_state_mode [GuiSequent.focused]
set_target [GuiSequent.focused]
set_title [Tactical.feedback]
Update the title wrt current selection & tuning
set_title [Wp.Tactical.feedback]
Update the title wrt current selection & tuning
set_value [GuiTactic.composer]
show [GuiList.pane]
simplify_branch [Conditions.simplifier]
Currently simplify a branch condition.
simplify_branch [Wp.Conditions.simplifier]
Currently simplify a branch condition.
simplify_exp [Conditions.simplifier]
Currently simplify an expression.
simplify_exp [Wp.Conditions.simplifier]
Currently simplify an expression.
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]
sort [Strategy.pool]
sort [Wp.Strategy.pool]
status [GuiProof.printer]

T
target [GuiTactic.browser]
target [GuiTactic.composer]
target [Conditions.simplifier]
Give the predicate that will be simplified later
target [Wp.Conditions.simplifier]
Give the predicate that will be simplified later
targeted [GuiTactic.tactic]
timeout [ProverTask.command]
title [GuiTactic.browser]
title [GuiTactic.composer]
title [Strategy.heuristic]
title [Tactical.composer]
title [Tactical.tactical]
title [Tactical.make]
title [Wp.Strategy.heuristic]
title [Wp.Tactical.composer]
title [Wp.Tactical.tactical]
title [Wp.Tactical.make]
tree [GuiProof.printer]

U
unselect [GuiSequent.focused]
update [GuiSource.highlighter]
update [GuiGoal.pane]
update [GuiProver.prover]
update [GuiList.pane]
update [GuiConfig.dp_button]
update_all [GuiList.pane]
update_field [Tactical.feedback]
Update field parameters
update_field [Wp.Tactical.feedback]
Update field parameters
updates [Pcond.state]

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]
vlemmas [Definitions.visitor]
Visit all lemmas
vlemmas [Wp.Definitions.visitor]
Visit all lemmas
vlibrary [Definitions.visitor]
vlibrary [Wp.Definitions.visitor]
vparam [Definitions.visitor]
vparam [Wp.Definitions.visitor]
vpred [Definitions.visitor]
vpred [Wp.Definitions.visitor]
vself [Definitions.visitor]
Visit all records, types, defs and lemmas
vself [Wp.Definitions.visitor]
Visit all records, types, defs and lemmas
vsymbol [Definitions.visitor]
vsymbol [Wp.Definitions.visitor]
vsymbols [Definitions.visitor]
Visit all definitions
vsymbols [Wp.Definitions.visitor]
Visit all definitions
vtau [Definitions.visitor]
vtau [Wp.Definitions.visitor]
vterm [Definitions.visitor]
vterm [Wp.Definitions.visitor]
vtype [Definitions.visitor]
vtype [Wp.Definitions.visitor]
vtypes [Definitions.visitor]
Visit all typedefs
vtypes [Wp.Definitions.visitor]
Visit all typedefs