4390.lean:6:4-6:13: warning: declaration uses `sorry`
4390.lean:6:0-11:19: warning: declaration uses `sorry`