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


          
            
            1038.lean:1:7-1:21: error: unknown constant 'IO.FS.realpath'