Repository navigation

fix(verdict): a bare constructor in a type goes to the kernel at its goal (#1619) - #1620

Merged

Lorenzobattistela merged 2 commits into

bendlang:mainfrom

ScottMoore0:fix-verdict-ctr-goal

Oct 16, 2026

Merged

fix(verdict): a bare constructor in a type goes to the kernel at its goal (#1619)#1620
Lorenzobattistela merged 2 commits into
bendlang:mainfrom
ScottMoore0:fix-verdict-ctr-goal

Commits on Oct 16, 2026
- fix(verdict): a bare constructor goes to the kernel at its goal, so a function in a parameter field goes η-long (#1619)
  
  ScottMoore0
  and
  claude
  committed
  9144e4e
- test(verdict): a generic constructor field at an erased or dependent function type (#1619)
  
  committed
  0f88b00