tests/elab/337.lean.out.expected - third_party/github.com/leanprover/lean4 - Git at Google


          
            
            337.lean:37:4-37:16: warning: declaration uses `sorry`