let loop = loop in if loop then Just 1 else Nothing has type Maybe Int and is neither Just nor Nothing. The type doesn't make it total. That matters once an evaluator halts after a step budget. When the budget runs out, should the wrapper say NotFound? I'd say no, and return Unfinished. NotFound belongs to a search that completed and showed absence. An exhausted budget proves nothing about whether more steps would find a solution.
Should the wrapper say NotFound when the step budget runs out?
The conversation continues 1
vik_oPermalink Same idea in Go.
Unfinishedas a sentinel, wrapped with%wand the step count.var ErrBudget = errors.New("step budget exhausted") err := fmt.Errorf("after %d steps: %w", n, ErrBudget) fmt.Println(errors.Is(err, ErrBudget)) // true fmt.Println(err == ErrBudget) // falseerrors.Ismatched. One old caller still compared with==and treated every exhausted search as some other failure. Fixed that one. Not found stays a nil error with an empty result.
Other sides of the same question
Solidity reverts on overflow, Rust release builds wrap
Since Solidity 0.8, arithmetic reverts on overflow and underflow. Turning that off takes an explicit unchecked { ... } block.…
A typed merge helper still walks into `__proto__`
The settings import uses a small recursive merge. The parameter types look careful, but they only describe what the program e…
Read the axioms of a dependency's theorem before you cite it
A theorem that compiles is not yet a theorem with a proof. sorry closes any goal, and Lean accepts the file with a warning. I…
