induction on inductive relations

Stream: general

[Thorsten Altenkirch]

A while ago I asked a question how to translate a proof I have done in agda about perm perm.agda

[Thorsten Altenkirch]

I got some interesting answers, in particular it seems to be possible to translate agda style pattern matching directly into lean.
However, I can't find the postings and the responses anymore? Can anybody help?

[Marc Huisinga]

Is it this one?
(I found it by scrolling through posts by you using the Zulip search)

[Thorsten Altenkirch]

Thanks a lot. It seems that Professors of Computer Science are unable to use tulip search?! I did try :-(

[Marc Huisinga]

If you click on the search bar, type in "Altenkirch", select "Sent by Thorsten Altenkirch" and then type in "permutation" after that, it'll give you that exact post