Andrej Dudenhefner

@yforster @fakusb The main results on TM are the `Arbitrary_to_Binary.v` compression and the `Single/StepTM.v` compression. For these, `Smpl` is not really necessary and I replaced the remaining `TM_Correct` code by...

> Oh no, this is probably going to fail until the opam package for MetaCoq is merged ([coq/opam-coq-archive#2288 (comment)](https://github.com/coq/opam-coq-archive/pull/2288#issuecomment-1239201703)), which in turn relies on a new release of MetaCoq ([MetaCoq/metacoq#748](https://github.com/MetaCoq/metacoq/pull/748))...

@yforster Note that `smpl` will not be necessary anymore with https://github.com/uds-psl/coq-library-undecidability/pull/176, which is ready.

I have two major comments. - The proposed `MM2` halting from `(1,(0,0))` is already part of the prior, ready-to-merge PR https://github.com/uds-psl/coq-library-undecidability/pull/169, and plays an important role there. - The present...

@DmxLarchey since TMs are working with Coq vector primitives and MMAs work with your vector primitives (`vec_pos`, `vec_change`) the code is more cumbersome than necessary due to conversions. I also...

> use the tools of the StdLib on them. By the same, I mean eg `Notation vec := Vector.t` Yes, `vec := Vector.t` definitely helps. Still, some functionality like `vec_pos`...

> If it where up to me, I would rewrite `Vector.nth` in the StdLib to match the code of `vec_pos` instead of the converse ;-) I proposed this change to...

@DmxLarchey are you ok with the added MMA files and additions to your vec library?

Additional use of this technique (equivalent to finite multiset extension) is e.g. showing normalization properties for the simply typed lambda-calculus based on a decreasing (multiset) measure (cf. [measure_lt_wf](https://github.com/tudo-seal/uniform-intersection/blob/dffc48044552886094bb2b2ccee377f47748935d/stlc_nf.v#L672)). Unfortunately, this...

> I'm in favour of changing the library to the weakest license possible: MIT. In the end, we want as many people as possible to use our library :) I...