## Stream: new members

### Topic: Type coercion ints to nats

#### Patrick Lutz (Jun 10 2020 at 23:33):

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

#### Patrick Lutz (Jun 10 2020 at 23:35):

Oh wait, maybe the answer is abs n

#### Jalex Stark (Jun 10 2020 at 23:36):

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

#### Jalex Stark (Jun 10 2020 at 23:36):

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

#### Patrick Lutz (Jun 10 2020 at 23:39):

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

indeed

#### Jalex Stark (Jun 10 2020 at 23:42):

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 (Jun 11 2020 at 06:26):

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

#### Kevin Buzzard (Jun 11 2020 at 06:30):

Quotient.lift is also a decent

#### Kevin Buzzard (Jun 11 2020 at 06:30):

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

#### Reid Barton (Jun 11 2020 at 12:14):

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.

Last updated: May 10 2021 at 00:31 UTC