xiaoxiangmoe

-- PTS-style First-order dependent types
-- usage examples

--------------------------------------------------------------------------------
-- λ→
def plus_1_of_nat : Π _ : ℕ, ℕ := λ x : ℕ, x + 1

#check plus_1_of_nat
#reduce Π _ : ℕ, ℕ