add proof for ¬ lex< xs [] ?

[mechvel]

Data.List.Relation.Lex.Core defines _<_ = Lex P _≈_ _≺_,

and I discover that \_ -> \lambda() does not prove ∀ xs → ¬ _<_ xs []
May be, it worth to add there (or somewhere)

 lex≮[] : ∀ xs → ¬ _<_ xs []
 lex≮[] [] (base ()) 

?

[gallais]

I'd write the type as ¬ (xs < []) and would call it xs≮[] but otherwise yes that seems reasonable.

[MatthewDaggitt]

Yup, I agree, useful addition and xs≮[] is the best name. @mechvel would you like to put together a pull request?

[mechvel]

@mechvel would you like to put together a pull request?

I do not understand (do not recall) what is a pull request.
Probably standard library has an administrator (Matthew?). Has it?
As he agrees with the proposal of

 xs≮[] : ∀ xs → ¬ (xs < [])
 xs≮[] [] (base ()) 

, then he adds this code to Data.List.Relation.Lex.Core for the next library version, and will add a notice to CHANGELOG.md.
Is this a way, for the library to develop?

[MatthewDaggitt]

@mechvel a pull request (PR) is exactly what we helped you through in #65. You may also find out how to prepare one in the HACKING file if you've forgotten.

Although I could do it myself, it works better if everyone else helps too. This way you yourself can contribute to the library, and in future can help make bigger changes such as incorporating your Bin library.

[mechvel]

@mechvel a pull request (PR) is exactly what we helped you through in #65. You may also find out
how to prepare one in the HACKING file if you've forgotten.

I had difficulties with pull request, was not able to accomplish it without your help.
After Agda + library becomes close enough to an official release, I shall decide whether to try to move with the Binary-4* proposal. Then I shall need to revisit the pull request matter (may be this will be easier this time, because I have now a fresh browser).

[jamesmckinna]

While I am at it: PR #1648 only resolved this issue for List. There's a corresponding lemma for Vec to add... another day.
Edited. There's a new branch issue602-vector open on my fork. Will open a PR when you can face it!

[jamesmckinna]

Hmmm. Those changes (on branch issue602-vector on jamesmckinna/agda-stdlib) now have horrible conflicts with the up-to-date agda/master branch. Will delete my branch, recreate it and then make a PR.
Edited. Now open as PR #1672.

[MatthewDaggitt]

Yes, if the changes you want to preserve are heavily localised to a single place then it's often easier to copy them across to a fresh branch rather than try to merge.