10234.lean:4:4-4:11: warning: declaration uses `sorry`
10234.lean:21:4-21:11: warning: declaration uses `sorry`