DecreasingCall.step: def of bend-lint-rules@0.2.0.0
Import: import bend-lint-rules@0.2.0.0/language/decreasing_call.bend as DecreasingCall
Lines 152-163 of bend-lint-rules@0.2.0.0/language/decreasing_call.bend: https://jend.leeeet.dev/read.txt?path=bend-lint-rules@0.2.0.0/language/decreasing_call.bend&start_line=152&end_line=163

import Base

# What one argument, a variable, says: none to read on (it is the parameter, unchanged), else the
# verdict: it decreases (a field a match took apart), the rule cannot tell (a let's name), or it fails.
def step(same: Bool, smaller: Bool, local: Bool, at: Nat, param: String) -> Maybe<&2, Verdict>:
  match same smaller local:
    case True{} _ _:
      None{}
    case False{} True{} _:
      Some{Decreases{}}
    case False{} False{} True{}:
      Some{Unknown{}}
    case False{} False{} False{}:
      Some{Fails{at, param}}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bend-lint-rules@0.2.0.0/language/decreasing_call.bend&name=Verdict