Index of class methods

A
add [GuiList.pane]
add [ProverTask.command]
add [Strategy.pool]
add [Wp.ProverTask.command]
add [Wp.Strategy.pool]
add_float [ProverTask.command]
add_float [Wp.ProverTask.command]
add_int [ProverTask.command]
add_int [Wp.ProverTask.command]
add_lemma [Generator.computer]
add_list [ProverTask.command]
add_list [Wp.ProverTask.command]
add_parameter [ProverTask.command]
add_parameter [Wp.ProverTask.command]
add_positive [ProverTask.command]
add_positive [Wp.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
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]
clear [Wp.Pcond.state]
coerce [GuiGoal.pane]
coerce [GuiList.pane]
command [ProverTask.command]
command [Wp.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]
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]
domain [Wp.Pcond.state]
F
field [Lang.idprinting]
field [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

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_after [Wp.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_float [Wp.ProverTask.pattern]
get_focus_mode [GuiSequent.focused]
get_int [ProverTask.pattern]
get_int [Wp.ProverTask.pattern]
get_state [Pcond.sequence]

If true, states are rendered when printing sequences.

get_state [Wp.Pcond.sequence]

If true, states are rendered when printing sequences.

get_state_mode [GuiSequent.focused]
get_string [ProverTask.pattern]
get_string [Wp.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]
hline [Wp.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_atomic_lv [Wp.Pcfg.engine]
is_valid [GuiTactic.composer]
iter_selected [GuiList.pane]
L
label_at [Pcond.state]
label_at [Wp.Pcond.state]
lemma [Generator.computer]
lines [ProverTask.printer]
lines [Wp.ProverTask.printer]
link [Lang.idprinting]
link [Wp.Lang.idprinting]
lookup [Plang.engine]
lookup [Wp.Plang.engine]
M
mark [Pcond.engine]

Marks terms to share in step

mark [Wp.Pcond.engine]

Marks terms to share in step

marks [Plang.engine]
marks [Wp.Plang.engine]
model [Generator.computer]
N
name [Pcond.engine]

Printer Components

name [Conditions.simplifier]
name [Wp.Pcond.engine]

Printer Components

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]
paragraph [Wp.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_addr [Wp.Pcfg.engine]
pp_at [Pcond.state]
pp_at [Wp.Pcond.state]
pp_atom [Pcfg.engine]
pp_atom [Vlist.engine]
pp_atom [Wp.Pcfg.engine]
pp_block [Pcond.engine]
pp_block [Wp.Pcond.engine]
pp_chunk [Pcfg.engine]

chunk name

pp_chunk [Wp.Pcfg.engine]

chunk name

pp_clause [Pcond.engine]

Default: "@{<wp:clause>...}"

pp_clause [Wp.Pcond.engine]

Default: "@{<wp:clause>...}"

pp_comment [Pcond.engine]

Default: "@{<wp:comment>(* ... *)}"

pp_comment [Wp.Pcond.engine]

Default: "@{<wp:comment>(* ... *)}"

pp_condition [Pcond.engine]
pp_condition [Wp.Pcond.engine]
pp_core [Pcond.engine]

Default: plang#pp_sort

pp_core [Wp.Pcond.engine]

Default: plang#pp_sort

pp_definition [Pcond.engine]
pp_definition [Wp.Pcond.engine]
pp_esequent [Pcond.engine]

Print the sequent in the given environment.

pp_esequent [Wp.Pcond.engine]

Print the sequent in the given environment.

pp_flow [Pcfg.engine]
pp_flow [Vlist.engine]
pp_flow [Wp.Pcfg.engine]
pp_goal [Pcond.engine]
pp_goal [Wp.Pcond.engine]
pp_host [Pcfg.engine]

current state

pp_host [Wp.Pcfg.engine]

current state

pp_intro [Pcond.engine]
pp_intro [Wp.Pcond.engine]
pp_label [Pcfg.engine]

label name

pp_label [Wp.Pcfg.engine]

label name

pp_lval [Pcfg.engine]

current state

pp_lval [Wp.Pcfg.engine]

current state

pp_main [GuiProof.printer]
pp_name [Pcond.engine]

Default: Format.pp_print_string

pp_name [Wp.Pcond.engine]

Default: Format.pp_print_string

pp_node [GuiProof.printer]
pp_offset [Pcfg.engine]
pp_offset [Wp.Pcfg.engine]
pp_ofs [Pcfg.engine]
pp_ofs [Wp.Pcfg.engine]
pp_pred [GuiSequent.focused]
pp_pred [Plang.engine]
pp_pred [Wp.Plang.engine]
pp_property [Pcond.engine]

Default: "@{<wp:property>(* ... *)}"

pp_property [Wp.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_sequence [Wp.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_sequent [Wp.Pcond.engine]

Print the sequent in global environment.

pp_step [Pcond.engine]

Assumes an "<hv>" box is opened.

pp_step [Wp.Pcond.engine]

Assumes an "<hv>" box is opened.

pp_stmt [Pcond.engine]

Default: "@{<wp:stmt>...}"

pp_stmt [Wp.Pcond.engine]

Default: "@{<wp:stmt>...}"

pp_term [GuiSequent.focused]
pp_update [Pcond.state]
pp_update [Wp.Pcond.state]
pp_value [Pcond.state]
pp_value [Wp.Pcond.state]
pp_warning [Pcond.engine]

Default: "@{<wp:warning>Warning}..."

pp_warning [Wp.Pcond.engine]

Default: "@{<wp:warning>Warning}..."

pretty [ProverTask.command]
pretty [Wp.ProverTask.command]
print [GuiComposer.browser]
print [GuiComposer.composer]
printf [ProverTask.printer]
printf [Wp.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]
run [Wp.ProverTask.command]
S
sanitize [Lang.idprinting]
sanitize [Wp.Lang.idprinting]
sanitize_field [Lang.idprinting]

Defulats to self#sanitize

sanitize_field [Wp.Lang.idprinting]

Defulats to self#sanitize

sanitize_fun [Lang.idprinting]

Defulats to self#sanitize

sanitize_fun [Wp.Lang.idprinting]

Defulats to self#sanitize

sanitize_type [Lang.idprinting]

Defaults to self#sanitize

sanitize_type [Wp.Lang.idprinting]

Defaults to self#sanitize

search [GuiTactic.browser]
search [Strategy.heuristic]
search [Wp.Strategy.heuristic]
section [ProverTask.printer]
section [Definitions.visitor]

Comment

section [Wp.ProverTask.printer]
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_command [Wp.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_domain [Wp.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_goal [Wp.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_sequence [Wp.Pcond.sequence]

Initialize state with this sequence

set_sequence [Wp.Pcond.state]
set_sequent [Pcond.sequence]

Set sequence and goal

set_sequent [Wp.Pcond.sequence]

Set sequence and goal

set_state [Pcond.sequence]

If set to false, states rendering is deactivated.

set_state [Wp.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]
timeout [Wp.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]
updates [Wp.Pcond.state]
V
vadt [Definitions.visitor]
vadt [Wp.Definitions.visitor]
validate_pattern [ProverTask.command]
validate_pattern [Wp.ProverTask.command]
validate_time [ProverTask.command]
validate_time [Wp.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