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


          
            
            matchOrIssue.lean:7:10-7:13: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected