lean4-htt/tests/lean/diamond5.lean.expected.out
2021-08-10 07:46:15 -07:00

1 line
155 B
Text

diamond5.lean:15:32-15:35: error: failed to create coercion 'D.toC' to parent structure 'C', environment already contains a declaration with the same name