---
name: Request for comments
about: Create a feature proposal
title: 'RFC: '
labels: RFC
assignees: ''

---

### Proposal

Clear and detailed description of the proposal. Consider the following questions:

  - **User Experience**: How does this feature improve the user experience?

  - **Beneficiaries**: Which Lean users and projects benefit most from this feature/change?

  - **Maintainability**: Will this change streamline code maintenance or simplify its structure?

### Community Feedback

Ideas should be discussed on [the Lean Zulip](https://leanprover.zulipchat.com) prior to submitting a proposal. Summarize all prior discussions and link them here.

### Impact

Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.
