sampleableExt

Mathlib.Testing.Plausible.Sampleable

URI: https://scilib.ai/kg/mathlib#Plausible.PNat.sampleableExt

Lean4

instance sampleableExt : SampleableExt PNat :=
  mkSelfContained
    (do
      let n ← chooseNat
      return Nat.succPNat n)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru