lean4-htt/tests/lean/structInst1.lean.expected.out

3 lines
114 B
Text

structInst1.lean:12:11-12:19: error: field 'toA' has already been specified
f5 : C → A → C
f6 : C → A → A