Commit 2025-10-28 10:18 0b502d55
View on Github →feat: CoeFun for Lex and Colex (#30481)
If F is a function type, we should be able to treat Lex F as a function type too. This diminishes the visual clutter of going to and from Lex.
This design was already present for pi types, but wasn't accounted for with neither of DFinsupp or Finsupp.