Skip to content

Commit

Permalink
fix(control/random): typo (#16156)
Browse files Browse the repository at this point in the history
Fix a small typo in the `random.lean` doc comment of `mk_generator` definition.
  • Loading branch information
oxarbitrage committed Aug 19, 2022
1 parent e8ca35f commit e1b7b7d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/control/random.lean
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ namespace io
private def accum_char (w : ℕ) (c : char) : ℕ :=
c.to_nat + 256 * w

/-- create and a seed a random number generator -/
/-- create and seed a random number generator -/
def mk_generator : io std_gen := do
seed ← io.rand 0 shift_31_left,
return $ mk_std_gen seed
Expand Down

0 comments on commit e1b7b7d

Please sign in to comment.