Zulip Chat Archive
Stream: general
Topic: preorder.lift
Reid Barton (Nov 28 2018 at 20:47):
I'm tempted to define lt explicitly in preorder.lift as \lam x y, f x < f y. Does this seem like a terrible idea for any obvious reason?
Reid Barton (Nov 28 2018 at 20:47):
The current definition does not play well with restricting a well ordering to a subtype
Mario Carneiro (Nov 28 2018 at 20:47):
that should be fine
Kenny Lau (Nov 28 2018 at 20:48):
more things to add to the PR limbo! :P
Reid Barton (Nov 28 2018 at 20:49):
:fencing:
Reid Barton (Nov 28 2018 at 21:07):
Nice, it didn't break anything, and solved my issue.
Last updated: Dec 20 2023 at 11:08 UTC