Zulip Chat Archive

Stream: new members

Topic: Understanding rec

Felipe (Nov 11 2022 at 07:03):

Hi I'm new to Lean/dependent types. I'm trying to understand the rec and rec_on eliminators in the non-trivial cases like https://stackoverflow.com/a/74397922/754254. Any good resources to recommend?

Felipe (Nov 11 2022 at 19:35):

I think I figured out what's going on, but would love some feedback on my thoughts! Posted as Q&A: https://proofassistants.stackexchange.com/q/1833/1808

Last updated: Dec 20 2023 at 11:08 UTC