自然数

module foundations.natural-number where

open import foundations.universe

自然数を定義する。

data ℕ : Type lzero where
  zero : ℕ
  suc : ℕ → ℕ

0や128といった自然数リテラルをℕ型の項として使うには、次のようなプラグマを使う。

{-# BUILTIN NATURAL ℕ #-}

_ : ℕ
_ =