lean2/tests/lean/quot_ind_bug.lean.expected.out

4 lines
46 B
Text
Raw Permalink Normal View History

ind c ⟦a⟧ : B ⟦a⟧
c a : B ⟦a⟧
c a