Zulip Chat Archive

Stream: general

Topic: preorder.lift'

Johan Commelin (May 08 2019 at 07:21):

How do people feel about adding

/-- version of preorder.lift which doesn't use type class inference -/
def lift' : preorder β  (α  β)  preorder α := @preorder.lift _ _

to mathlib? We use it twice in the perfectoid project. But we can of course also use @preorder.lift _ _ .
(And yes, we are quite sure we don't want to use type class instances for these preorders, because we are looking at something like the type of all preorders on a ring that satisfy blah...)

If we add this to mathlib, I guess we also want partial_order.lift' etc, etc...

Mario Carneiro (May 08 2019 at 07:28):

I think you can just replace preorder.lift with this. It's usually used to create instances, so having a by apply_instance in there doesn't seem so bad

Mario Carneiro (May 08 2019 at 07:29):

I would put the preorder argument second though

Johan Commelin (May 08 2019 at 07:31):

Probably breaks a lot of files... and I don't have VScode atm (-; But let me see what I can do...

Johan Commelin (May 08 2019 at 07:47):

#995 -- let's see what Travis says. This PR was produced using grep and vim, without running Lean...

Johan Commelin (May 08 2019 at 07:54):

And... I failed. Travis doesn't like it

Johan Commelin (May 08 2019 at 11:05):

Hurray, after several iterations #995 passes the checks on Travis. (And I never ran Lean locally :grimacing:)

Last updated: Dec 20 2023 at 11:08 UTC