Daniel Nezamabadi

As a side note, I am not sure where I can find the documentation for the meaning of the columns. The only reference I could find was #587 which links...

@jcp19 This problem came up when doing experiments on the examples from chapter 10.2 of Program Proofs, so I think AdtEncoding.scala. Additionally, perhaps SlicesImpl.scala, ArrayImpl.scala, Option(ToSeq)Impl.scala and StringEncoding.scala could be...

Do we want to keep this open, or should we close it in favor of the other issues/the project overview?

Came across this myself as well. Debug info: ``` AnkiDroid Version = 2.20.1 (e32a82c33646807ea19623c9c88be38965bc07e6) Backend Version = 0.1.48-anki24.11 (24.11 c47638ca36f99dd4f3b81ae82d964aec66e392e0) Android Version = 13 (SDK 33) ProductFlavor = play Manufacturer...

TL;DR: Cannot reproduce on newest beta As suggested by @mikehardy , I tried to reproduce after updating to the beta. I updated by signing up to the beta on Google...

Thanks for the reply! 1-tuples wouldn't be difficult to deal with, since CakeML support them AFAIK. The only "issue" that I can currently think of is that printing them might...

For discussions on concrete proposals, we are currently using topics prefixed with `[Refactor]` on [#❄️ HOL4](https://hol.zulipchat.com/#narrow/channel/486798-.E2.9D.84.EF.B8.8F-HOL4).

Fully updating to the new Quote syntax depends on https://github.com/HOL-Theorem-Prover/HOL/issues/1313 - in particular, there is at least once instance in `characteristic/examples/cf_examplesScript.sml` that is affected by this.

Closing in favor of more specific issues such as #1263.

To my understanding, `open` and thus by extension `Import` as suggested by @myreen would essentially "import" everything, i.e. instead of `baz.foo`, foo would be accessible directly via `foo`. I find...