Assumes the hypothesis
Generate VCs for all functions matching provided behaviors and property names.
Generate VCs for call preconditions at the given statement.
request-for-update event
Currently simplify a branch condition.
Currently simplify an expression.
Called after assuming hypothesis and knowing the goal
get_after ~offset:p k returns the end of the message starting p characters after the end of group k.
get_after ~offset:p k
p
k
If true, states are rendered when printing sequences.
true
Retrieve the title
Retrieve the errors
Add new hypotheses implied by the original hypothesis.
Interactive mode.
Marks terms to share in step
Generate VCs for the given Property.
Printer Components
Outer cluster to import
This local compinfo must be defined
This local function must be defined
This local lemma must be defined
This local compinfo initialization must be defined
External library to import
This local type must be defined
Global fresh variable pool
chunk name
Default: "@{<wp:clause>...}"
"@{<wp:clause>...}"
Default: "@{<wp:comment>(* ... *)}"
"@{<wp:comment>(* ... *)}"
Default: plang#pp_sort
plang#pp_sort
Print the sequent in the given environment.
current state
label name
Default: Format.pp_print_string
Format.pp_print_string
Default: "@{<wp:property>(* ... *)}"
"@{<wp:property>(* ... *)}"
Assumes an "<hv>" box is opened and all variables are declared.
Print the sequent in global environment.
Assumes an "<hv>" box is opened.
Default: "@{<wp:stmt>...}"
"@{<wp:stmt>...}"
Default: "@{<wp:warning>Warning}..."
"@{<wp:warning>Warning}..."
Edit enabled provers
Defulats to self#sanitize
self#sanitize
Defaults to self#sanitize
Comment
Shall return Applicable or Not_configured if the tactic might apply to the selection.
Applicable
Not_configured
send f calls f with the current value via the signal lock.
send f
f
Add a short description wrt current selection & tuning
Default is sequence's domain
Mark the current configuration as invalid
Adds goal to state domain
Initialize state with this sequence
Set sequence and goal
If set to false, states rendering is deactivated.
false
Update the title wrt current selection & tuning
Simplify the goal.
Give the predicate that will be simplified later
Update field parameters
Visit all lemmas
Visit all records, types, defs and lemmas
Visit all definitions
Visit all typedefs
Currently simplify an hypothesis before assuming it.