Stream: new members
Topic: boolean reflection in lean
Tobias Grosser (Sep 07 2018 at 06:26):
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 (Sep 07 2018 at 06:28):
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
Last updated: May 14 2021 at 03:27 UTC