show_term auto bound interaction and by?
alexjbest opened this issue · 0 comments
alexjbest commented
def t : {a : Nat} → Nat :=
by
intro X
sorry
works, but
def t : {a : Nat} → Nat :=
show_term by
intro X
sorry
auto introduces a as it is a term now and so breaks the proof.
Does this mean that the implementation of rw? should rather be as rw show_term instead of the other way around. I can't think of a downside but I'm not sure