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

:fencing:

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