Skip to content

Commit

Permalink
chore: drop some dead code (#259)
Browse files Browse the repository at this point in the history
This avoids a warning about the deprecated Std.BitVec
  • Loading branch information
tobiasgrosser authored Apr 24, 2024
1 parent 1635ad9 commit e7ab160
Showing 1 changed file with 3 additions and 6 deletions.
9 changes: 3 additions & 6 deletions SSA/Core/Util.lean
Original file line number Diff line number Diff line change
Expand Up @@ -113,22 +113,19 @@ instance [inst : Cli.ParseableType τ] {n : ℕ} : Cli.ParseableType (Vector τ
else
none


@[simp] abbrev Std.BitVec.width : Std.BitVec w → Nat := fun _ => w

/-- productsList [xs, ys] = [(x, y) for x in xs for y in ys],
extended to arbitary number of arrays. -/
def productsList : List (List α) -> List (List α)
| [] => [[]] -- empty product returns empty tuple.
| (xs::xss) => Id.run do
| (xs::xss) => Id.run do
let mut out := []
let xss' := productsList xss -- make tuples of the other columns.
for x in xs do -- for every element in this column, take product with all other tuples.
out := out.append (xss'.map (fun xs => x :: xs))
return out

example : productsList [["a"], ["x", "y", "z"]] = [["a", "x"], ["a", "y"], ["a", "z"]] := rfl
example : productsList [["a"], ["p", "q"], ["x", "y", "z"]] =
example : productsList [["a"], ["p", "q"], ["x", "y", "z"]] =
[["a", "p", "x"], ["a", "p", "y"], ["a", "p", "z"],
["a", "q", "x"], ["a", "q", "y"], ["a", "q", "z"]] := rfl

Expand Down

0 comments on commit e7ab160

Please sign in to comment.