Find points in a definition with a particular type

Stream: metaprogramming / tactics

[William Sørensen]

I have a situation where i have an Term of a given type, I want to find all points at which within subterms it has another type lets say given the prior defn:

def CoList.cons : {α : Type} → α → CoList α → CoList α := ...

and the term .cons n x : CoList nat, if the type I am looking for is CoList nat then it would yield the entire term and x, is something like this possible or should I try to take a different approach?

The reasons behind why I want to do this are quite strange but also fun, I need to transform applications of constructors like CoList.cons hd tl with this transformed structure Other.cons hd (.inr tl) and i do not quite know how to go about doing this in practice.

[William Sørensen]

Also would this be possible with Exprs maybe instead of Terms as I am aware there is type infrastructure for these at least. Anything really goes

[Anand Rao Tadipatri]

@William Sørensen Would docs#Lean.Meta.kabstract be useful here? This can be used to replace all occurrences of a certain pattern in an expression with another one. This function is used in implementing Lean's rw tactic.

[William Sørensen]

thanks for the tip, i will take a look. I ended up making this goofy function that uses unification to detect where it would be required but i wasnt able to finish it as i had some situations where a partially applied expression would unify but not the raw expression, maybe this would be useful though

[Anand Rao Tadipatri]

Maybe you could apply each partially applied expression to meta-variable arguments and then try unifying.

[William Sørensen]

This is what i am currently trying, but i dont know if unification would be able to figure out the dependent type thats needed. well see though

[Chris Bailey]

Can you just use https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.Expr.foldlM to replace, and the appropriate meta functions for type inference and checking what the constructor application is, etc.? You walk (and can map) over all subterms during the fold and just see whether they're applications of .cons and replace them if they are.