Update docs: EasyCrypt/easycrypt@0096d84

Author: github-actions[bot]

refman/tactics/simplify-if.html

@@ -163,7 +163,7 @@ <h1>Tactic: <code class="docutils literal notranslate"><span class="pre">simplif
       "goals":[
         "Type variables: <none>\n\nj_: int\n------------------------------------------------------------------------\nContext : hr: {j, i, x, y : int}\n\npre = j = j_\n\n\npost =\n  if 0 = j then\n    if 1 = j then\n      if 2 = j then\n        if 3 = j then\n          if 4 = j then\n            if 5 = j then\n              (5, 0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, 0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y0 = 0 + 4 in\n            if 5 = j then\n              (5, y0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (3, y0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n        else\n          let y0 = 0 + 3 in\n          if 4 = j then\n            if 5 = j then\n              (5, y0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y1 = y0 + 4 in\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (2, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n      else\n        let y0 = 0 + 2 in\n        if 3 = j then\n          if 4 = j then\n            if 5 = j then\n              (5, y0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y1 = y0 + 4 in\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (3, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n        else\n          let y1 = y0 + 3 in\n          if 4 = j then\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y2 = y1 + 4 in\n            if 5 = j then\n              (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (1, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n    else\n      let y0 = 0 + 1 in\n      if 2 = j then\n        if 3 = j then\n          if 4 = j then\n            if 5 = j then\n              (5, y0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y1 = y0 + 4 in\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (3, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n        else\n          let y1 = y0 + 3 in\n          if 4 = j then\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y2 = y1 + 4 in\n            if 5 = j then\n              (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (2, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n      else\n        let y1 = y0 + 2 in\n        if 3 = j then\n          if 4 = j then\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y2 = y1 + 4 in\n            if 5 = j then\n              (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (3, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n        else\n          let y2 = y1 + 3 in\n          if 4 = j then\n            if 5 = j then\n              (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y3 = y2 + 4 in\n            if 5 = j then\n              (5, y3) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (0, y3 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n  else\n    if 1 = j then\n      if 2 = j then\n        if 3 = j then\n          if 4 = j then\n            if 5 = j then\n              (5, 0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, 0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y0 = 0 + 4 in\n            if 5 = j then\n              (5, y0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (3, y0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n        else\n          let y0 = 0 + 3 in\n          if 4 = j then\n            if 5 = j then\n              (5, y0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y1 = y0 + 4 in\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (2, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n      else\n        let y0 = 0 + 2 in\n        if 3 = j then\n          if 4 = j then\n            if 5 = j then\n              (5, y0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y1 = y0 + 4 in\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (3, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n        else\n          let y1 = y0 + 3 in\n          if 4 = j then\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y2 = y1 + 4 in\n            if 5 = j then\n              (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (1, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n    else\n      let y0 = 0 + 1 in\n      if 2 = j then\n        if 3 = j then\n          if 4 = j then\n            if 5 = j then\n              (5, y0) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y0 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y1 = y0 + 4 in\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (3, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n        else\n          let y1 = y0 + 3 in\n          if 4 = j then\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y2 = y1 + 4 in\n            if 5 = j then\n              (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (2, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n      else\n        let y1 = y0 + 2 in\n        if 3 = j then\n          if 4 = j then\n            if 5 = j then\n              (5, y1) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y1 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y2 = y1 + 4 in\n            if 5 = j then\n              (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (3, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n        else\n          let y2 = y1 + 3 in\n          if 4 = j then\n            if 5 = j then\n              (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (4, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n          else\n            let y3 = y2 + 4 in\n            if 5 = j then\n              (5, y3) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n            else (0, y3 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n\n"
       ],
-      "message":"info: time: 0.001029"
+      "message":"info: time: 0.001037"
     },
     {
       "goals":[
@@ -286,7 +286,7 @@ <h2><a class="toc-backref" href="#id1" role="doc-backlink">Variant: Transform at
       "goals":[
         "Type variables: <none>\n\nj_: int\n------------------------------------------------------------------------\nContext : hr: {j, i, x, y : int}\n\npre = j = j_\n\n\npost =\n  let tpl =\n    let x0 = 0 in\n    let y0 = 0 in (if 0 = j then x0 else 0, if 0 = j then 0 else y0) in\n  let y0 = tpl.`2 in\n  if 1 = j then\n    let tpl0 =\n      let x0 = 2 in\n      let y1 = y0 + 2 in (if 2 = j then x0 else 1, if 2 = j then y0 else y1)\n    in\n    let y1 = tpl0.`2 in\n    if 3 = j then\n      let tpl1 =\n        let x0 = 4 in\n        let y2 = y1 + 4 in\n        (if 4 = j then x0 else 3, if 4 = j then y1 else y2) in\n      let y2 = tpl1.`2 in\n      if 5 = j then (5, y2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n      else (tpl1.`1, y2 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n    else\n      let y2 = y1 + 3 in\n      let tpl1 =\n        let x0 = 4 in\n        let y3 = y2 + 4 in\n        (if 4 = j then x0 else tpl0.`1, if 4 = j then y2 else y3) in\n      let y3 = tpl1.`2 in\n      if 5 = j then (5, y3) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n      else (tpl1.`1, y3 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n  else\n    let y1 = y0 + 1 in\n    let tpl0 =\n      let x0 = 2 in\n      let y2 = y1 + 2 in\n      (if 2 = j then x0 else tpl.`1, if 2 = j then y1 else y2) in\n    let y2 = tpl0.`2 in\n    if 3 = j then\n      let tpl1 =\n        let x0 = 4 in\n        let y3 = y2 + 4 in\n        (if 4 = j then x0 else 3, if 4 = j then y2 else y3) in\n      let y3 = tpl1.`2 in\n      if 5 = j then (5, y3) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n      else (tpl1.`1, y3 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n    else\n      let y3 = y2 + 3 in\n      let tpl1 =\n        let x0 = 4 in\n        let y4 = y3 + 4 in\n        (if 4 = j then x0 else tpl0.`1, if 4 = j then y3 else y4) in\n      let y4 = tpl1.`2 in\n      if 5 = j then (5, y4) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n      else (tpl1.`1, y4 + 5) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n\n"
       ],
-      "message":"info: time: 0.000332"
+      "message":"info: time: 0.000344"
     },
     {
       "goals":[
@@ -385,7 +385,7 @@ <h2><a class="toc-backref" href="#id2" role="doc-backlink">Variant: Transform as
       "goals":[
         "Type variables: <none>\n\nj_: int\n------------------------------------------------------------------------\nContext : hr: {j, i, x, y : int}\n\npre = j = j_\n\n\npost =\n  let tpl =\n    let x0 = 0 in\n    let y0 = 0 in (if 0 = j then x0 else 0, if 0 = j then 0 else y0) in\n  let y0 = tpl.`2 in\n  let tpl0 =\n    let x0 = 1 in\n    let y1 = y0 + 1 in\n    (if 1 = j then x0 else tpl.`1, if 1 = j then y0 else y1) in\n  let y1 = tpl0.`2 in\n  let tpl1 =\n    let x0 = 2 in\n    let y2 = y1 + 2 in\n    (if 2 = j then x0 else tpl0.`1, if 2 = j then y1 else y2) in\n  let y2 = tpl1.`2 in\n  let tpl2 =\n    let x0 = 3 in\n    let y3 = y2 + 3 in\n    (if 3 = j then x0 else tpl1.`1, if 3 = j then y2 else y3) in\n  let y3 = tpl2.`2 in\n  let tpl3 =\n    let x0 = 4 in\n    let y4 = y3 + 4 in\n    (if 4 = j then x0 else tpl2.`1, if 4 = j then y3 else y4) in\n  let y4 = tpl3.`2 in\n  let tpl4 =\n    let x0 = 5 in\n    let y5 = y4 + 5 in\n    (if 5 = j then x0 else tpl3.`1, if 5 = j then y4 else y5) in\n  (tpl4.`1, tpl4.`2) = if 0 <= j_ < 6 then (j_, 15 - j_) else (0, 15)\n\n"
       ],
-      "message":"info: time: 0.000118"
+      "message":"info: time: 0.000119"
     },
     {
       "goals":[