mirror of
https://github.com/Smaug123/CubicalTutorial
synced 2025-10-05 16:08:40 +00:00
14 lines
229 B
Agda
14 lines
229 B
Agda
{-# OPTIONS --safe --warning=error --without-K #-}
|
||
|
||
module Naturals where
|
||
|
||
data ℕ : Set where
|
||
zero : ℕ
|
||
succ : ℕ → ℕ
|
||
|
||
{-# BUILTIN NATURAL ℕ #-}
|
||
|
||
_+N_ : ℕ → ℕ → ℕ
|
||
zero +N b = b
|
||
succ a +N b = succ (a +N b)
|