Zulip Chat Archive

Stream: new members

Topic: Type coercion ints to nats


view this post on Zulip 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?

view this post on Zulip Patrick Lutz (Jun 10 2020 at 23:35):

Oh wait, maybe the answer is abs n

view this post on Zulip Jalex Stark (Jun 10 2020 at 23:36):

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

view this post on Zulip Jalex Stark (Jun 10 2020 at 23:36):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 10 2020 at 23:41):

indeed

view this post on Zulip 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

view this post on Zulip Patrick Stevens (Jun 11 2020 at 06:26):

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

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 06:30):

Quotient.lift is also a decent

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 06:30):

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

view this post on Zulip 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