Lean的类型宇宙

2023年08月16日 02:20
#check Nat.succ     -- NatNat
#check (0, 1)       -- Nat × Nat
#check Nat.add      -- NatNatNat

#check Nat.succ 2   -- Nat
#check Nat.add 3    -- NatNat
#check Nat.add 5 2  -- Nat
#check (5, 9).1     -- Nat
#check Nat               -- Type
#check Bool              -- Type
#check NatBool        -- Type
#check Nat × Bool        -- Type
#check NatNat         -- ...
#check Nat × NatNat
#check NatNatNat
#check Nat → (NatNat)
#check NatNatBool
#check (NatNat) → Nat
def α : Type := Nat
def β : Type := Bool
def F : TypeType := List
def G : TypeTypeType := Prod

#check α        -- Type
#check F α      -- Type
#check F Nat    -- Type
#check G α      -- TypeType
#check G α β    -- Type
#check G α Nat  -- Type
#check Type     -- Type 1
#check Type 1   -- Type 2
#check Type 2   -- Type 3
#check Type 3   -- Type 4
#check Type 4   -- Type 5
Code

```js
#check Nat.succ     -- Nat → Nat
#check (0, 1)       -- Nat × Nat
#check Nat.add      -- Nat → Nat → Nat

#check Nat.succ 2   -- Nat
#check Nat.add 3    -- Nat → Nat
#check Nat.add 5 2  -- Nat
#check (5, 9).1     -- Nat
#check Nat               -- Type
#check Bool              -- Type
#check Nat → Bool        -- Type
#check Nat × Bool        -- Type
#check Nat → Nat         -- ...
#check Nat × Nat → Nat
#check Nat → Nat → Nat
#check Nat → (Nat → Nat)
#check Nat → Nat → Bool
#check (Nat → Nat) → Nat
def α : Type := Nat
def β : Type := Bool
def F : Type → Type := List
def G : Type → Type → Type := Prod

#check α        -- Type
#check F α      -- Type
#check F Nat    -- Type
#check G α      -- Type → Type
#check G α β    -- Type
#check G α Nat  -- Type
#check Type     -- Type 1
#check Type 1   -- Type 2
#check Type 2   -- Type 3
#check Type 3   -- Type 4
#check Type 4   -- Type 5
```