Zulip Chat Archive

Stream: general

Topic: preorder.lift


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

view this post on Zulip Reid Barton (Nov 28 2018 at 20:47):

The current definition does not play well with restricting a well ordering to a subtype

view this post on Zulip Mario Carneiro (Nov 28 2018 at 20:47):

that should be fine

view this post on Zulip Kenny Lau (Nov 28 2018 at 20:48):

more things to add to the PR limbo! :P

view this post on Zulip Reid Barton (Nov 28 2018 at 20:49):

:fencing:

view this post on Zulip Reid Barton (Nov 28 2018 at 21:07):

Nice, it didn't break anything, and solved my issue.


Last updated: May 11 2021 at 00:31 UTC