Small Scale Reflection for the Working Lean User

Vladimir Gladshtein, George Pîrlea, Ilya Sergey

We present the design and implementation of the Small Scale Reflection proof methodology and tactic language (a.k.a. SSR) for the Lean 4 proof assistant. Like its Coq predecessor S…