[ fix #432 #460 ] Heterogeneous version of Sublist #562
Conversation
We are getting close to having all the features we used to have in the purely propositional version.
This builds locally so this time it should be fine! :D
|
This last stretch is so boring I seem to only make progress when I'm stuck on a train. |
gallais
changed the title
src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
Outdated
Show resolved
Hide resolved
|
|
||
| module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where | ||
|
|
||
| tail-Sublist : ∀ {as bs} → Pointwise R as bs → |
There was a problem hiding this comment.
These properties should all use the +/- notation rather than having Sublist in the name.
There was a problem hiding this comment.
I don't think they should: Sublist (drop n xs) xs is not the same as Sublist xs ys -> Sublist (drop n xs) (drop n ys).
There was a problem hiding this comment.
Okay tail is special because it's in that first form. The rest are all in the second form though right?
There was a problem hiding this comment.
The other ones are in the shape Sublist as bs -> Sublist (f as) bs. The function is only
applied to the first one (it's a generalisation of Sublist (f xs) xs which is useful when
the R relation Sublist is built upon is not transitive.
I guess I forgot to generalise tail-Sublist too! :D
There was a problem hiding this comment.
Ah okay, makes sense now. This is probably one of the cases mentioned in #595 where the notation is too compact to be readable. It's not like they need to be compatible somewhere else and writing out the full types would definitely help!
There was a problem hiding this comment.
I'll inline the notations & add comments to the section header to explain
the distinction.
There was a problem hiding this comment.
What would your thoughts be on calling them tail-sublist or tail-isSublist rather than tail-Sublist? Nitpicky I know.
There was a problem hiding this comment.
I was reusing these names: take-⊆ et al..
Whatever we pick, we should also apply the same convention to things like
≤⇒pred≤ : ∀ {m n} → m ≤ n → pred m ≤ n
(and document it).
There was a problem hiding this comment.
Hmm maybe you're right and tail-Sublist is fine...
|
I'm happy to have a go at this @gallais? |
|
I didn't switch it to ready because we have the ongoing discussion about names. |
|
Ah sorry I'd missed your commit fixing the |
|
I am now getting errors on open import Data.List.Relation.Binary.Sublist.Propositional.Properties public using (⊆-refl; ⊆-trans)Where to find these functions now? (Answer: they are now named |
The design of
First,Prefix, etc. has now informed the way I seeSublist.So I have bitten the bullet and decided to build this heterogeneous version.
In the end, this will actually make #460 irrelevant (so I'm closing that one).
Still missing: