Skip to content

Updates available but manual intervention required #2546

Description

@github-actions

Try lake update and then investigate why this update causes lake build, lake test, or lake lint to fail.
Files changed in update:

  • lake-manifest.json
  • lean-toolchain

Build Output

✖ [3055/3514] Building LeanByExample.Option.SkipKernelTC (1.6s)
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Option/SkipKernelTC.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Option/SkipKernelTC.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Option/SkipKernelTC.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Option/SkipKernelTC.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Option/SkipKernelTC.setup.json --json
error: LeanByExample/Option/SkipKernelTC.lean:46:55: Unknown constant `USize.thmDecl`

Note: Inferred this name from the expected resulting type of `.thmDecl`:
  USize
error: LeanByExample/Option/SkipKernelTC.lean:47:6: Type mismatch
  Except.ok env
has type
  Except ?m.12 ?m.11
but is expected to have type
  Option IO.CancelToken → Except Kernel.Exception Environment
error: LeanByExample/Option/SkipKernelTC.lean:53:8: Unknown identifier `bad_proof₂.elim`
info: LeanByExample/Option/SkipKernelTC.lean:57:0: 'easy_proof₂' depends on axioms: [sorryAx]
error: LeanByExample/Option/SkipKernelTC.lean:56:0: ❌️ Docstring on `#guard_msgs` does not match generated message:

- info: 'easy_proof₂' does not depend on any axioms
+ info: 'easy_proof₂' depends on axioms: [sorryAx]
error: Lean exited with code 1
✖ [3561/3564] Building LeanByExample.TypeClass.BEq (575ms)
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/TypeClass/BEq.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/TypeClass/BEq.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/TypeClass/BEq.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/TypeClass/BEq.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/TypeClass/BEq.setup.json --json
info: LeanByExample/TypeClass/BEq.lean:52:0: inferInstance : DecidableEq Float
error: LeanByExample/TypeClass/BEq.lean:52:0: unexpected success
error: Lean exited with code 1
✖ [3562/3564] Building LeanByExample.Diagnostic.Whnf (991ms)
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Diagnostic/Whnf.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Diagnostic/Whnf.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Diagnostic/Whnf.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Diagnostic/Whnf.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Diagnostic/Whnf.setup.json --json
info: LeanByExample/Diagnostic/Whnf.lean:75:0: @[instance_reducible] def instManyFunctor : Functor Many :=
inferInstance
error: LeanByExample/Diagnostic/Whnf.lean:74:0: ❌️ Docstring on `#guard_msgs` does not match generated message:

- info: @[implicit_reducible] def instManyFunctor : Functor Many :=
+ info: @[instance_reducible] def instManyFunctor : Functor Many :=
  inferInstance
error: Lean exited with code 1
✖ [3563/3564] Building LeanByExample.EXTRA.SelectionSort (1.2s)
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/EXTRA/SelectionSort.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/EXTRA/SelectionSort.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/EXTRA/SelectionSort.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/EXTRA/SelectionSort.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/EXTRA/SelectionSort.setup.json --json
info: LeanByExample/EXTRA/SelectionSort.lean:23:19: failed to synthesize instance of type class
  Std.IsLinearOrder α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
error: LeanByExample/EXTRA/SelectionSort.lean:89:16: `grind` failed
case grind.1.2.1.2.2.1
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
inst_2 : DecidableEq α
inst_3 : Std.IsLinearPreorder α
head : α
tail : List α
h : ¬(head :: tail).minFirst ~ head :: tail
w : α
h_2 : ¬count w (head :: tail).minFirst = count w (head :: tail)
h_3 : -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
h_4 : ¬-1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
h_5 : (head :: tail).min ⋯ = w
h_6 : ¬head = w
h_7 : ¬-1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
left : (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
right :
  ∀ (a : α),
    count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
      count a ((head :: tail).erase ((head :: tail).min ⋯))
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] Std.IsLinearPreorder α
    [prop] ¬(head :: tail).minFirst ~ head :: tail
    [prop] ((head :: tail).minFirst ~ head :: tail) =
          ∀ (a : α), count a (head :: tail).minFirst = count a (head :: tail)
    [prop] (head :: tail).minFirst = (head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)
    [prop] ¬count w (head :: tail).minFirst = count w (head :: tail)
    [prop] (head :: tail).minFirst ~ head :: tail →
          (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
    [prop] (head :: tail).erase ((head :: tail).min ⋯) =
          if head = (head :: tail).min ⋯ then tail else head :: tail.erase ((head :: tail).min ⋯)
    [prop] (head :: tail).minFirst ~ head :: tail → count w (head :: tail).minFirst = count w (head :: tail)
    [prop] count w (head :: tail) = count w tail + if head = w then 1 else 0
    [prop] count w ((head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)) =
          count w ((head :: tail).erase ((head :: tail).min ⋯)) + if (head :: tail).min ⋯ = w then 1 else 0
    [prop] ((head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)) =
          ∀ (a : α),
            count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
              count a ((head :: tail).erase ((head :: tail).min ⋯))
    [prop] ((head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)).erase ((head :: tail).min ⋯) =
          (head :: tail).erase ((head :: tail).min ⋯)
    [prop] (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯) →
          count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
            count w ((head :: tail).erase ((head :: tail).min ⋯))
    [prop] count w ((head :: tail).erase ((head :: tail).min ⋯)) =
          count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0
    [prop] ↑(count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0) =
          if -1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
            ↑(count w (head :: tail)) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
          else 0
    [prop] count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
          count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0
    [prop] ↑(count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0) =
          if -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
            ↑(count w (head :: tail).minFirst) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
          else 0
    [prop] -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
    [prop] ¬-1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
    [prop] (head :: tail).min ⋯ = w
    [prop] ¬head = w
    [prop] count w (head :: tail.erase ((head :: tail).min ⋯)) =
          count w (tail.erase ((head :: tail).min ⋯)) + if head = w then 1 else 0
    [prop] count w (tail.erase ((head :: tail).min ⋯)) = count w tail - if (head :: tail).min ⋯ = w then 1 else 0
    [prop] ↑(count w tail - if (head :: tail).min ⋯ = w then 1 else 0) =
          if -1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
            ↑(count w tail) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
          else 0
    [prop] ¬-1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
    [prop] (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
    [prop] ∀ (a : α),
          count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
            count a ((head :: tail).erase ((head :: tail).min ⋯))
    [prop] count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
          count w ((head :: tail).erase ((head :: tail).min ⋯))
  [eqc] True propositions
    [prop] Std.IsLinearPreorder α
    [prop] -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
    [prop] ¬head :: tail = []
    [prop] ((head :: tail).minFirst ~ head :: tail) =
          ∀ (a : α), count a (head :: tail).minFirst = count a (head :: tail)
    [prop] (head :: tail).min ⋯ = w
    [prop] (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
    [prop] (head :: tail).minFirst ~ head :: tail → count w (head :: tail).minFirst = count w (head :: tail)
    [prop] (head :: tail).minFirst ~ head :: tail →
          (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
    [prop] ((head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)) =
          ∀ (a : α),
            count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
              count a ((head :: tail).erase ((head :: tail).min ⋯))
    [prop] count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
          count w ((head :: tail).erase ((head :: tail).min ⋯))
    [prop] ∀ (a : α),
          count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
            count a ((head :: tail).erase ((head :: tail).min ⋯))
    [prop] (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯) →
          count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
            count w ((head :: tail).erase ((head :: tail).min ⋯))
  [eqc] False propositions
    [prop] (head :: tail).minFirst ~ head :: tail
    [prop] -1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
    [prop] -1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
    [prop] count w (head :: tail).minFirst = count w (head :: tail)
    [prop] head :: tail = []
    [prop] ∀ (a : α), count a (head :: tail).minFirst = count a (head :: tail)
    [prop] head = w
    [prop] head = (head :: tail).min ⋯
  [eqc] Equivalence classes
    [eqc] {(head :: tail).minFirst, (head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)}
    [eqc] {w, (head :: tail).min ⋯}
    [eqc] {count w (head :: tail), count w tail + if head = w then 1 else 0}
    [eqc] {count w (head :: tail).minFirst,
        1,
        count w ((head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)),
        count w ((head :: tail).erase ((head :: tail).min ⋯)) + if (head :: tail).min ⋯ = w then 1 else 0}
      [eqc] {if (head :: tail).min ⋯ = w then 1 else 0}
    [eqc] {(head :: tail).erase ((head :: tail).min ⋯),
        head :: tail.erase ((head :: tail).min ⋯),
        (head :: tail).minFirst.erase ((head :: tail).min ⋯),
        ((head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)).erase ((head :: tail).min ⋯)}
      [eqc] {if head = (head :: tail).min ⋯ then tail else head :: tail.erase ((head :: tail).min ⋯)}
    [eqc] {count w ((head :: tail).erase ((head :: tail).min ⋯)),
        count w (head :: tail.erase ((head :: tail).min ⋯)),
        count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)),
        count w (tail.erase ((head :: tail).min ⋯)) + if head = w then 1 else 0,
        count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0,
        count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0}
    [eqc] {count w (tail.erase ((head :: tail).min ⋯)), count w tail - if (head :: tail).min ⋯ = w then 1 else 0}
    [eqc] others
      [eqc] {↑0,
          ↑(count w (tail.erase ((head :: tail).min ⋯))),
          ↑(count w ((head :: tail).erase ((head :: tail).min ⋯))),
          ↑(if head = w then 1 else 0),
          0,
          if -1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
            ↑(count w tail) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
          else 0,
          if -1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
            ↑(count w (head :: tail)) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
          else 0,
          if -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
            ↑(count w (head :: tail).minFirst) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
          else 0,
          ↑(count w (head :: tail).minFirst) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0),
          ↑(count w (tail.erase ((head :: tail).min ⋯)) + if head = w then 1 else 0),
          ↑(count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0),
          ↑(count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0),
          ↑(count w tail - if (head :: tail).min ⋯ = w then 1 else 0)}
      [eqc] {↑(if (head :: tail).min ⋯ = w then 1 else 0),
          ↑1,
          ↑(count w (head :: tail).minFirst),
          ↑(count w ((head :: tail).erase ((head :: tail).min ⋯)) + if (head :: tail).min ⋯ = w then 1 else 0)}
      [eqc] {0, if head = w then 1 else 0}
      [eqc] {-1 * ↑(count w (head :: tail).minFirst), -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)}
      [eqc] {↑(count w ((head :: tail).erase ((head :: tail).min ⋯))),
          ↑(if head = w then 1 else 0),
          ↑(count w (tail.erase ((head :: tail).min ⋯))),
          ↑(count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0),
          ↑(count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0),
          ↑(count w tail - if (head :: tail).min ⋯ = w then 1 else 0)}
      [eqc] {↑(count w (head :: tail)), ↑(count w tail + if head = w then 1 else 0)}
  [cases] Case analyses
    [cases] [1/2]: if -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
          ↑(count w (head :: tail).minFirst) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
        else 0
      [cases] source: E-matching `count_erase`
    [cases] [2/2]: if -1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
          ↑(count w (head :: tail)) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
        else 0
      [cases] source: E-matching `count_erase`
    [cases] [1/2]: if (head :: tail).min ⋯ = w then 1 else 0
      [cases] source: E-matching `count_cons`
    [cases] [2/2]: if head = w then 1 else 0
      [cases] source: E-matching `count_cons`
    [cases] [2/2]: if -1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
          ↑(count w tail) + -1 * ↑(if (head ::...(truncated)

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions