Zulip Chat Archive

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

Jalex Stark (Jun 10 2020 at 23:41):

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: Dec 20 2023 at 11:08 UTC