def StateValue.valid.go

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

import Base

1776# `char` is a value character followed by `tail`, of which at most `room`
1777# characters are allowed; the last character is not a space.
1778def StateValue.valid.go(tail: String, char: Char, room: Nat) -> Bool:
1779  match tail:
1780    case SNil{}:
1781      StateChar.is_value_end(char)
1782    case SCon{next, rest}:
1783      match room:
1784        case 0n:
1785          False{}
1786        case 1n+left:
1787          Bool.and(StateChar.is_value(char), StateValue.valid.go(rest, next, left))