Skip to content

Commit 5efb5c7

Browse files
committed
Apply suggestions from code review
Remove extra `[g ⊢ _]` arguments in `fstep_impl_red`
1 parent b35b21d commit 5efb5c7

File tree

1 file changed

+8
-8
lines changed

1 file changed

+8
-8
lines changed

case-studies/harmony-lemma-formalization/5_theorem1.bel

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -195,22 +195,22 @@ fn f ⇒ case f of
195195
| [g ⊢ fs_par2 F2] ⇒ let [g ⊢ R] = fstep_impl_red [g ⊢ F2] in
196196
[g ⊢ r_str par_comm (r_par R) par_comm]
197197
| [g ⊢ fs_com1 F1 B1] ⇒
198-
let [g ⊢ D1] = fs_out_rew [g ⊢ _] [g ⊢ F1] in
199-
let [g ⊢ D2] = bs_in_rew [g ⊢ _] [g ⊢ B1] in
198+
let [g ⊢ D1] = fs_out_rew [g ⊢ F1] in
199+
let [g ⊢ D2] = bs_in_rew [g ⊢ B1] in
200200
let [g ⊢ R] = fs_com1_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R]
201201
| [g ⊢ fs_com2 B1 F1] ⇒
202-
let [g ⊢ D1] = bs_in_rew [g ⊢ _] [g ⊢ B1] in
203-
let [g ⊢ D2] = fs_out_rew [g ⊢ _] [g ⊢ F1] in
202+
let [g ⊢ D1] = bs_in_rew [g ⊢ B1] in
203+
let [g ⊢ D2] = fs_out_rew [g ⊢ F1] in
204204
let [g ⊢ R] = fs_com2_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R]
205205
| [g ⊢ fs_res \z.F[..,z]] ⇒
206206
let [g,z:names ⊢ R[..,z]] = fstep_impl_red [g,z:names ⊢ F[..,z]] in
207207
[g ⊢ r_res \z.R[..,z]]
208208
| [g ⊢ fs_close1 B1 B2] ⇒
209-
let [g ⊢ D1] = bs_out_rew [g ⊢ _][g ⊢ B1] in
210-
let [g ⊢ D2] = bs_in_rew [g ⊢ _] [g ⊢ B2] in
209+
let [g ⊢ D1] = bs_out_rew [g ⊢ B1] in
210+
let [g ⊢ D2] = bs_in_rew [g ⊢ B2] in
211211
let [g ⊢ R] = fs_close1_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R]
212212
| [g ⊢ fs_close2 B1 B2] ⇒
213-
let [g ⊢ D1] = bs_in_rew [g ⊢ _] [g ⊢ B1] in
214-
let [g ⊢ D2] = bs_out_rew [g ⊢ _] [g ⊢ B2] in
213+
let [g ⊢ D1] = bs_in_rew [g ⊢ B1] in
214+
let [g ⊢ D2] = bs_out_rew [g ⊢ B2] in
215215
let [g ⊢ R] = fs_close2_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R]
216216
;

0 commit comments

Comments
 (0)