1 paper
Jonathan Sterling
The syntax and semantics of user-supplied hypothesis names in tactic languages is a thorny problem, because the binding structure of a proof is a function of the goal at which a ta…