Lean中let可以在所有宇宙里生效

2023年08月16日 02:14

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

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

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

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