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


          
            
            eraseSimp.lean:4:18-4:21: warning: 'foo' does not have [simp] attribute