English
There exists a sampling method for Rat by choosing an integer d within a symmetric interval and a natural n within a bound, then producing the ratio d/n.
Русский
Существует метод выборки рациональных, который выбирает целое d в симметричном интервале и натуральное n в пределах границы, затем получает отношение d/n.
LaTeX
$$$\exists d\in \mathbb{Z},\; \exists n\in \mathbb{N},\; -m\le d\le m\;\wedge\; 0\le n\le m\Rightarrow \text{sample} = \mathrm{Rat.divInt}(d,n)$$$
Lean4
instance sampleableExt : SampleableExt Rat :=
mkSelfContained
(do
let d ←
choose Int (-(← getSize)) (← getSize)
(le_trans (Int.neg_nonpos_of_nonneg (Int.ofNat_zero_le _)) (Int.ofNat_zero_le _))
let n ← choose Nat 0 (← getSize) (Nat.zero_le _)
return Rat.divInt d n)
