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


          
            
            ellipsisProjIssue.lean:1:17: error: unexpected `.` immediately after `..`