.lean_options