Open david-christiansen opened 1 month ago
Some entries with long namespace could be further grouped by the last namespaces, e.g. String.*, Nat.*, Lean.Elab.Tactic.*, Lean.Meta.Simp.*.
String.*
Nat.*
Lean.Elab.Tactic.*
Lean.Meta.Simp.*
Some entries with long namespace could be further grouped by the last namespaces, e.g.
String.*,Nat.*,Lean.Elab.Tactic.*,Lean.Meta.Simp.*.