def step

bend-lint-rules@0.2.0.0 · language/decreasing_call.bend:152

import Base

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