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


            
            435.lean:3:0-3:7: warning: declaration uses 'sorry'

            
            435.lean:5:21-5:23: error: unknown identifier 'op' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
	435.lean:3:0-3:7: warning: declaration uses 'sorry'
	435.lean:5:21-5:23: error: unknown identifier 'op' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.