Michael Norrish
Michael Norrish
The particularly simple theorems look like good candidates for `simp`.
Strictly, `v2w` and `v2n` don't conflict: they have different types and don't refer to each other. If the issue is how to deal with `or` on words and its connection...
Are you planning to finalise this (make it not a draft)?
This will get done as part of the wider project to BNF-ify our datatype definition package. I'll add that issue and make this a sub-part (which should amount to making...
In fact, the existing #266 is that overarching issue.
It’s not obvious to me that it is overly cluttered (and removing MEM made it less cluttered of course :-). The complete list of constants is ``` ALL_DISTINCT :α list...
I didn't mean to denigrate `ZIP`; it would just be better in ListPair (as per the Basis). I also like mapPartial, so would be more than happy to see it...
Yes, a `features/better-lists` branch or something would be the way to go. But what’s the plan of work? Is it just: 1. move pair-ish constants to new `listPairTheory` 2. add...
Totally agree about providing a `LEX` relation. What would be a good name for a theory that included `PAD_LEFT`? And where would `SNOC` go? ((Half-seriously) We could just make `SNOC`...