Skip to content

Commit

Permalink
add Array.allSubsts function
Browse files Browse the repository at this point in the history
  • Loading branch information
lecopivo committed Oct 3, 2024
1 parent 3ef9d9a commit 883f600
Showing 1 changed file with 14 additions and 0 deletions.
14 changes: 14 additions & 0 deletions SciLean/Lean/Array.lean
Original file line number Diff line number Diff line change
Expand Up @@ -111,3 +111,17 @@ def colexOrd {α} [Ord α] (as bs : Array α) : Ordering := Id.run do
| .gt => return .gt
| .eq => continue
return .eq


/-- Return array of all subarrays of the input array. -/
def allSubsets {α} (a : Array α) : Array (Array α) := Id.run do
let mut as : Array (Array α) := #[]
let n := a.size
for i in [0:2^n] do
let mut ai : Array α := #[]
for h : j in [0:a.size] do
if (2^j).toUInt64 &&& i.toUInt64 ≠ 0 then
ai := ai.push (a[j])

as := as.push ai
return as

0 comments on commit 883f600

Please sign in to comment.