@@ -14,6 +14,7 @@ weakest precondition can grow exponentially:
1414
1515.. ecproof ::
1616 :title: Weakest precondition grows exponentially.
17+
1718 require import AllCore.
1819
1920 module M = {
@@ -41,14 +42,15 @@ weakest precondition can grow exponentially:
4142 smt().
4243 qed.
4344
45+ Since the tactic preserves semantics, it can be applied to all program logics.
46+
4447.. admonition :: Syntax
45- Since the tactic preserves semantics, it can be applied to all program logics.
4648
47- `simplify if side? codepos? `
49+ `simplify if side? codepos? `
4850
49- The `side ` argument is required when the goal is an `equiv ` judgment; it specifies
51+ The `side ` argument is required when the goal is an `equiv ` judgment; it specifies
5052on which side the transformation should be applied.
51- The `codepos ` argument allows you to indicate which `if ` statement the transformation
53+ The `codepos ` argument allows you to indicate which `if ` statement the transformation
5254should target.
5355
5456.. contents ::
@@ -59,8 +61,10 @@ Variant: Transform at a given code possition
5961------------------------------------------------------------------------
6062The tactic applies only if the branches of the selected `if ` statement consist solely of
6163assignments.
62- .. exproof ::
63- : title: Hoare logic example selecting where to apply the transformation
64+
65+ .. ecproof ::
66+ :title: Hoare logic example selecting where to apply the transformation.
67+
6468 require import AllCore.
6569
6670 module M = {
@@ -104,7 +108,7 @@ This variant attempts to find a position where the transformation can be applied
104108applies it. The process is repeated until no applicable position remains.
105109
106110.. ecproof ::
107- :title: Hoare logic example
111+ :title: Hoare logic example.
108112
109113 require import AllCore.
110114
0 commit comments