def nat_in_defect

bend-schema-lib@0.4.1.0 · core.bend:971

import Base

971# The same two reasons at an SNatIn and an SBool, replayed along a path: the
972# value's own kind is the defect when the path ends here, and it is not a
973# defect at all further along (the walk passed it).
974def nat_in_defect(+lo: Nat, +hi: Nat, r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
975  match r p:
976    case RNum{+n} Nil{}:
977      guard(Bool.not(num_ok(lo, hi, n)), Some{NotIn{lo, hi}})
978    case RNum{n} st <> q:
979      None{}
980    case x Nil{}:
981      Some{missing_or(x, NotNat{})}
982    case x st <> q:
983      None{}