G. Allais
G. Allais
I am not sure what the point of top level functions with quantity `1` is but this does appear to be inconsistent.
@jamesmckinna In that last commit I think you forgot to add the moved file so it just looks like you nuked everything. As for the naming debate, I would say...
While trying to cleanup `insert-swap-≤` (without much success), I proved a few auxiliary things that may be useful: ```agda insert-spec : ∀ x xs → insert x xs ≋ takeWhile...
If you chase various definitions you can see: ```idris -- In Idris.IDEMode.REPL process (DocsFor n modeOpt) = replWrap $ Idris.REPL.process (Doc $ APTerm (PRef EmptyFC (UN $ mkUserName n))) ```...
Marking as abandoned for now.
I thought it was already in the style guide as @MatthewDaggitt has been pushing for `contradiction` over `⊥-elim` pretty consistently in the past.
```agda _∪_ : ∀ {l} → (xs ys : Sublist l) → Sublist l _∩_ : ∀ {l} → (xs ys : Sublist l) → Sublist l ``` Ooooh fancy....
I was thinking about that but we have `Relation.Unary` rather than `Predicate`. So for consistency we should maybe reorganise the whole `Data.List.Relation` into `Data.List.Relation.Unary` and `Data.List.Relation.Binary`? We could maintain backwards...
There's a feature freeze at the moment so the answer is no. Plus I'm currently making sure I finally ship my thesis. :D But I may find the time to...
`Sublist` is more general surely?