Meme of LinOnetwo

def foo := let a := Nat; fun x : a => x + 2

TS里变量宇宙的用let，类型宇宙的得用 type；但是Lean里全部用let即可。