Complement predicate

Stream: Is there code for X?

[Wrenna Robson]

What's the standard spelling for the complement permutation if the order hierarchy isn't imported (so I can't use complement permutation)?

[Aaron Liu]

What's the complement permutation?

[Wrenna Robson]

Oh! I mean predicate.

[Wrenna Robson]

Permutations on the brain.

[Edward van de Meent]

what does complement have to do with order?

[Edward van de Meent]

complement is a set operation...
EDIT: TIL, it generalizes to lattices n stuff, which ofc is an order-theoretic concept

[Wrenna Robson]

I don't know but that appears to be where I found the notation...

[Aaron Liu]

fun a => ¬p a?

[Wrenna Robson]

Yes.

[Aaron Liu]

I think that's just how you spell it

[Wrenna Robson]

Right - I mean that's fine too!

[Aaron Liu]

maybe (¬p ·) if you want to be shorter

[Wrenna Robson]

Yes that's probably what I'd do

[Edward van de Meent]

/me has gained knowledge about complement as a concept in order theory

[Wrenna Robson]

I just kinda want to be able to write \not p

[Wrenna Robson]

docs#Not

[Eric Wieser]

(¬p .)?

[Wrenna Robson]

I think that's the nicest spelling.

[Wrenna Robson]

Short of having a notation for it and we do once the HasCompl instance kicks in I guess.

[Eric Wieser]

The hascompl instance is probably a bad choice, since it's syntactically different.

[Eric Wieser]

It's probably also not simp-normal