## Stream: general

### Topic: preorder.lift'

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

/-- 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: May 14 2021 at 07:19 UTC