lean4-htt/tests/lean/structInstError.lean.expected.out
2020-12-24 09:35:55 -08:00

2 lines
113 B
Text

structInstError.lean:5:7: error: invalid {...} notation, expected type is not known
{ x := 10, b := true } : Foo