def StateKey.valid.rest

bend-trace-context@0.2.0.0 · trace_context.bend:1753

import Base

1753# Every remaining character is a key character, and at most `room` remain.
1754# The recursion stops once the room is used up, so a huge invalid key is not
1755# read to its end.
1756def StateKey.valid.rest(text: String, room: Nat) -> Bool:
1757  match text:
1758    case SNil{}:
1759      True{}
1760    case SCon{char, tail}:
1761      match room:
1762        case 0n:
1763          False{}
1764        case 1n+left:
1765          Bool.and(StateChar.is_key(char), StateKey.valid.rest(tail, left))