boolean reflection in lean

Stream: new members

[Tobias Grosser]

I am currently looking into a coq proof that is heavily based on ssreflect. Being new to lean, I wonder if there is some counterpart in lean I should have a look at.

[Simon Hudon]

Proof by reflection is currently a weak part of Lean. I think Lean 4 will solve that but for now, it is not an effective technique for Lean