Return a certified positive natural exactly when the input is positive.
4 lines · Lean 4
Objectifs
- Return a certified positive natural exactly when the input is positive.
Indices
Voir la solution
def PositiveNat := {n : Nat // 0 < n}
def PositiveNat.ofNat? (n : Nat) : Option PositiveNat := by
if h : 0 < n then
exact some ⟨n, h⟩
else
exact none