rec_on

Stream: lean4

[Dean Young]

What happened to eq.rec_on in Lean 4?

[Dean Young]

I thought it would become Eq.rec_on but that doesn't work.

What is a motive? I think I have one, that I want to demonstrate extensionality for these dependent structures.

[Alex J. Best]

It's Eq.recOn now

[Dean Young]

@Alex J. Best Can you link me to some documentation for it?

[Alex J. Best]

I don't know anything specifically for Eq.recOn but it works in the same way as other recursors which you can read about in https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html (and the chapter after)

[Alex J. Best]

If you look at docs#Eq you can read a bit about how equality is defined inductively

[Richard Copley]

https://xenaproject.wordpress.com/2021/04/18/induction-on-equality/ is also fun