lean2/tests/lean/quot_ind_bug.lean

7 lines
169 B
Text
Raw Permalink Normal View History

open quot
variables {A : Type} [s : setoid A] {B : quot s → Prop} (c : ∀ (a : A), B (quot.mk a)) (a : A)
check quot.ind c ⟦a⟧
check c a
eval quot.ind c ⟦a⟧