pattern matching wrapped in Option

Stream: lean4

[Horatiu Cheval]

Not really a question, but I am amazed by the fact that this works

inductive TType where
| natural : TType
| application : TType → TType → TType
deriving DecidableEq

infixr:60 "↣" => TType.application
open TType

def inferType : Option TType → Option TType → Option TType
| ρ ↣ τ, σ => if ρ = σ then some τ else none
| _, _ => none

#reduce inferType (natural ↣ natural ↣ natural) natural
-- some (natural↣natural)

#reduce inferType natural natural
-- none

#reduce inferType none natural
none