Type coercion ints to nats

Stream: new members

[Patrick Lutz]

If I have n : ℤ and h : n ≥ 0 how do I get a term k of type ℕ such that (k : ℤ) = n?

[Patrick Lutz]

Oh wait, maybe the answer is abs n

[Jalex Stark]

if you're in tactic mode lift n to \N using h might be useful

[Jalex Stark]

it should consume h and give you k : \N with hk : \u k = n

[Patrick Lutz]

feels funny to say "lift n from the integers to the natural numbers," feels more like a descent

[Jalex Stark]

indeed

[Jalex Stark]

it's not hard to define an instance of can_lift for yourself in case you run into a situation where you want it to work and it doesnt

[Patrick Stevens]

There's also int.to_nat which returns 0 for n < 0.

[Kevin Buzzard]

Quotient.lift is also a decent

[Kevin Buzzard]

Computer scientists don't seem to think about these things in the same way

[Reid Barton]

But lifting from integers to natural numbers really is lifting--you have N -> Z and k : Z and you want to get something in N.