Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Dec 2, 2024
1 parent 8cc788e commit d64043d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Plausible/Gen.lean
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ def listOf (x : Gen α) : Gen (List α) := do
/-- Given a list of example generators, choose one to create an example. -/
def oneOf (xs : Array (Gen α)) (pos : 0 < xs.size := by decide) : Gen α := do
let ⟨x, _, h2⟩ ← up <| chooseNatLt 0 xs.size pos
xs.get ⟨x, h2⟩
xs[x]

/-- Given a list of examples, choose one to create an example. -/
def elements (xs : List α) (pos : 0 < xs.length) : Gen α := do
Expand Down

0 comments on commit d64043d

Please sign in to comment.