PR !4#9040: feat: `to_snoc` an attribute for generating l...

Stream: triage

[Random Issue Bot]

Today I chose PR 9040 for discussion!

feat: to_snoc an attribute for generating lemmas with snoc in them
Created by @Bolton Bailey (@BoltonBailey) on 2023-12-13
Labels: help-wanted, WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose PR 9040 for discussion!

feat: to_snoc an attribute for generating lemmas with snoc in them
Created by @Bolton Bailey (@BoltonBailey) on 2023-12-13
Labels: help-wanted, WIP, please-adopt, t-meta

Is this PR still relevant? Any recent updates? Anyone making progress?

[Bolton Bailey]

I haven’t worked on mathlib for a while, so no progress has been made. Nevertheless, I think it’s a good idea that someone could potentially adopt.