def cite

bolt@1.27.0.0 · src/rules/style/transcong.bend:119

import Base
import bolt@1.27.0.0/src/finding.bend as F

119# the finding at the `Equal.trans` leaf
120def cite(+ll: U32, +cc: U32, +path: String) -> F.Finding:
121  F.Finding{path, ll, cc, 11, "transcong",
122    "this Equal.trans is fed an Equal.cong: rewrite instead, `%e : {F(_) == c : T}` with the other proof below it, which names the motive once and drops the middle term."}