6467.lean:4:8-4:10: warning: declaration uses `sorry`