file name & docs

leanprover-community · Jun 9, 2024 · 612d756 · 612d756
1 parent efef3df
commit 612d756
Showing 1 changed file with 14 additions and 2 deletions.
diff --git a/Batteries/Data/Nat/Bitwise.lean → Batteries/Data/Nat/BinaryRec.lean b/Batteries/Data/Nat/Bitwise.lean → Batteries/Data/Nat/BinaryRec.lean
@@ -1,7 +1,19 @@
 /-
-Copyright (c) 2024 Yuyang Zhao. All rights reserved.
+Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yuyang Zhao
+Authors: Praneeth Kolichala, Yuyang Zhao
+-/
+
+/-!
+# Binary recursion on `Nat`
+
+This file defines binary recursion on `Nat`.
+
+## Main results
+* `Nat.binaryRec`: A recursion principle for `bit` representations of natural numbers.
+* `Nat.binaryRec'`: The same as `binaryRec`, but the induction step can assume that if `n=0`,
+  the bit being appended is `true`.
+* `Nat.binaryRecFromOne`: The same as `binaryRec`, but special casing both 0 and 1 as base cases.
 -/
 
 namespace Nat