synthInstsIssue.lean:58:8-58:17: warning: declaration uses `sorry`