Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix(library/init/meta/tactic.lean): turn comment into docstring (#646)
This seems to be a slip, rather than a deliberate decision to not make the comment above `subst_core` into its docstring. It's very rare that I try to read meta code, but today I was trying to understand how `subst` worked and ran into the fact that `subst_core` had no docstring.
- Loading branch information