option.induction

Stream: general

[Kevin Buzzard]

I'm thinking about teaching materials. Is this definition OK? Would it be the sort of thing one can find in mathlib? Mathematicians find the word recursion a bit scary maybe.

[Kevin Buzzard]

def option.induction :  Π {X : Sort*} {C : option X → Prop},
C none → (Π (val : X), C (some val)) → Π (n : option X), C n
:= @option.rec

[Kevin Buzzard]

option.rec mentions Sort, and mathematicians do not believe in Sort.

[Kevin Buzzard]

Induction and recursion are two separate things to them.

[Kevin Buzzard]

What is the cool type theory name of this function:λ A B C D, F A B D C?

[David Wärn]

((∘) flip) ∘ F?

[Mario Carneiro]

a pointless hobby, I see

[David Wärn]

(∘) (∘) (∘) $ flip F is a more symmetric version