def proofy

bolt@1.27.0.0 · src/rules/suspicious/empty.bend:309

import Base
import bolt@1.27.0.0/src/syntax/lex.bend as Lex

309# is the def these tokens head (after `def`) a proof? Its tokens are read to
310# the bracket that closes its parameters, at depth zero; fin carries whether
311# the last token read was that bracket
312def proofy(toks: List<&2, Lex.Tok>, +dd: Nat, fin: Bool) -> Bool:
313  match toks:
314    case Nil{}:
315      False{}
316    case Con{Lex.Tok{+k, t, l, c}, +rest}:
317      match fin:
318        case True{}:
319          proofy.end(Lex.Tok{k, t, l, c} <> rest)
320        case False{}:
321          proofy(rest, close.depth(k, dd), proofy.fin(k, dd))