Assumes the hypothesis
request-for-update event
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.
Specify the field to use in an infoprover
Interactive mode.
Marks terms to share in step
Printer Components
Outer cluster to import
This local compinfo must be defined
This local function must be defined
This local lemma must be defined
External library to import
This local type must be defined
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
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
Currently simplify a branch condition.
Currently simplify an expression.
Simplify the goal.
Currently simplify an hypothesis before assuming it.
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