mirror of
https://github.com/anoma/juvix.git
synced 2024-12-14 08:27:03 +03:00
20 lines
193 B
Plaintext
20 lines
193 B
Plaintext
module M;
|
||
|
||
inductive ℕ {
|
||
z : ℕ;
|
||
s : ℕ → ℕ;
|
||
};
|
||
|
||
nat : Type;
|
||
nat := ℕ;
|
||
|
||
nat2 : Type;
|
||
nat2 := nat;
|
||
|
||
infixl 1 +;
|
||
+ : nat2 → nat → nat;
|
||
+ z b := b;
|
||
+ (s a) b := s (a + b);
|
||
|
||
end;
|