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

4 lines
180 B
Text

structure_elab_segfault.lean:1:0: error: infer type failed, sort expected
delayed[?m_1]
structure_elab_segfault.lean:2:0: error: infer type failed, sort expected
delayed[?m_1]