feat(library/init/data): add uint16 and make sure uint* - uses wraparound semantics like most programming languages

library/init/data/fin/basic.lean

@@ -47,15 +47,15 @@ protected def add : fin n → fin n → fin n
 protected def mul : fin n → fin n → fin n
 | ⟨a, h⟩ ⟨b, _⟩ := ⟨(a * b) % n, mlt h⟩
 
+protected def sub : fin n → fin n → fin n
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨(a + (n - b)) % n, mlt h⟩
+
 /-
 Remark: sub/mod/div can be defined without using (% n), but
 we are trying to minimize the number of nat theorems
 needed to boostrap Lean.
 -/
 
-protected def sub : fin n → fin n → fin n
-| ⟨a, h⟩ ⟨b, _⟩ := ⟨(a - b) % n, mlt h⟩
-
 protected def mod : fin n → fin n → fin n
 | ⟨a, h⟩ ⟨b, _⟩ := ⟨(a % b) % n, mlt h⟩
 

library/init/data/repr.lean

@@ -128,6 +128,9 @@ instance : has_repr string :=
 instance (n : nat) : has_repr (fin n) :=
 ⟨λ f, repr (fin.val f)⟩
 
+instance : has_repr uint16 :=
+⟨λ n, repr (fin.val n)⟩
+
 instance : has_repr uint32 :=
 ⟨λ n, repr (fin.val n)⟩
 

library/init/data/to_string.lean

@@ -51,6 +51,9 @@ instance : has_to_string char :=
 instance (n : nat) : has_to_string (fin n) :=
 ⟨λ f, to_string (fin.val f)⟩
 
+instance : has_to_string uint16 :=
+⟨λ n, to_string (fin.val n)⟩
+
 instance : has_to_string uint32 :=
 ⟨λ n, to_string (fin.val n)⟩
 

library/init/data/uint.lean

@@ -7,12 +7,19 @@ prelude
 import init.data.fin.basic
 
 open nat
+def uint16_sz : nat := 65536
+def uint16 := fin uint16_sz
+
 def uint32_sz : nat := 4294967296
 def uint32 := fin uint32_sz
 
 def uint64_sz : nat := 18446744073709551616
 def uint64 := fin uint64_sz
 
+instance : decidable_eq uint16 :=
+have decidable_eq (fin uint16_sz), from fin.decidable_eq _,
+this
+
 instance : decidable_eq uint32 :=
 have decidable_eq (fin uint32_sz), from fin.decidable_eq _,
 this
@@ -21,6 +28,16 @@ instance : decidable_eq uint64 :=
 have decidable_eq (fin uint64_sz), from fin.decidable_eq _,
 this
 
+instance : has_zero uint16 := ⟨fin.of_nat 0⟩
+instance : has_one uint16  := ⟨fin.of_nat 1⟩
+instance : has_add uint16  := ⟨fin.add⟩
+instance : has_sub uint16  := ⟨fin.sub⟩
+instance : has_mul uint16  := ⟨fin.mul⟩
+instance : has_mod uint16  := ⟨fin.mod⟩
+instance : has_div uint16  := ⟨fin.div⟩
+instance : has_lt uint16   := ⟨fin.lt⟩
+instance : has_le uint16   := ⟨fin.le⟩
+
 instance : has_zero uint32 := ⟨fin.of_nat 0⟩
 instance : has_one uint32  := ⟨fin.of_nat 1⟩
 instance : has_add uint32  := ⟨fin.add⟩
@@ -41,6 +58,12 @@ instance : has_div uint64  := ⟨fin.div⟩
 instance : has_lt uint64   := ⟨fin.lt⟩
 instance : has_le uint64   := ⟨fin.le⟩
 
+def uint16.of_nat (n : nat) : uint16 :=
+fin.of_nat n
+
+def uint16.to_nat (u : uint16) : nat :=
+fin.val u
+
 def uint32.of_nat (n : nat) : uint32 :=
 fin.of_nat n