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
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