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


            
            689.lean:2:14-4:7: error: unexpected token 'section'; expected '|'

            
            689.lean:9:0: error: unexpected end of input; expected '{'
	689.lean:2:14-4:7: error: unexpected token 'section'; expected '\|'
	689.lean:9:0: error: unexpected end of input; expected '{'