Empty.proofy.head: def of bolt@1.27.0.0
Import: import bolt@1.27.0.0/src/rules/suspicious/empty.bend as Empty
Lines 276-285 of bolt@1.27.0.0/src/rules/suspicious/empty.bend: https://jend.leeeet.dev/read.txt?path=bolt@1.27.0.0/src/rules/suspicious/empty.bend&start_line=276&end_line=285

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

# what the two tokens after a def's parameters say: a `:` (no type: the
# def fills a law) or `->` then `{` (it returns a proof)
def proofy.head(k1: Lex.TokKind, +k2: Lex.TokKind, +t2: String) -> Bool:
  match k1:
    case Lex.TColon{}:
      True{}
    case Lex.TArrow{}:
      String.eq(code(k2, t2), "{")
    case other:
      False{}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.eq
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/rules/suspicious/empty.bend&name=code
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/syntax/lex.bend&name=TokKind