Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: add Data.Fin.Coding and Data.Fin.Enum #1007

Draft
wants to merge 9 commits into
base: main
Choose a base branch
from
+848 −0
Draft

feat: add Data.Fin.Coding and Data.Fin.Enum #1007

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
8412201
feat: add Data.Fin.Coding and Data.Fin.Enum
fgdorais Sep 23, 2024
aef9392
chore: use encode/decode
fgdorais Oct 25, 2024
146f718
feat: make find? tail recursive
fgdorais Oct 25, 2024
401211b
chore: fix long line
fgdorais Oct 25, 2024
4e209ef
chore: cleanup
fgdorais Oct 25, 2024
9927b6c
feat: add instance for `Char`
fgdorais Oct 26, 2024
344a54b
chore: merge main
fgdorais Dec 2, 2024
c9d7790
chore: merge main
fgdorais Feb 8, 2025
2b8b7ac
chore: adaptations
fgdorais Feb 8, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Batteries/Data/Fin.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
import Batteries.Data.Fin.Basic
import Batteries.Data.Fin.Coding
import Batteries.Data.Fin.Enum
import Batteries.Data.Fin.Fold
import Batteries.Data.Fin.Lemmas
import Batteries.Data.Fin.OfBits
16 changes: 16 additions & 0 deletions Batteries/Data/Fin/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,3 +91,19 @@ This is the dependent version of `Fin.foldl`. -/
@[inline] def dfoldl (n : Nat) (α : Fin (n + 1) → Type _)
(f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) :=
dfoldlM (m := Id) n α f init

/-- Sum of a list indexed by `Fin n`. -/
protected def sum [OfNat α (nat_lit 0)] [Add α] (x : Fin n → α) : α :=
foldr n (x · + ·) 0

/-- Product of a list indexed by `Fin n`. -/
protected def prod [OfNat α (nat_lit 1)] [Mul α] (x : Fin n → α) : α :=
foldr n (x · * ·) 1

/-- Count the number of true values of a decidable predicate on `Fin n`. -/
protected def count (P : Fin n → Prop) [DecidablePred P] : Nat :=
Fin.sum (if P · then 1 else 0)

/-- Find the first true value of a decidable predicate on `Fin n`, if there is one. -/
protected def find? (P : Fin n → Prop) [DecidablePred P] : Option (Fin n) :=
foldr n (fun i v => if P i then some i else v) none
Loading
Loading