tomsib2001

Thanks for the quick answer! Now I know there's a reason for it.

Same issue on Koka 2.4.2, Ubuntu 20.04

I was able to fix this locally by simply calling the LLM again when there is a Parse error. I am sure my code is not exactly in the spirit...

I hope it's not too silly an idea, and looking at the code I'm not sure where such an intervention would take place, but: How about, instead of raising the...

Thank you very much for this very detailed answer! I will definitely look into it. EDIT: removed comment about four color theorem, it seems to already be there, just need...

The most advanced branch in terms of complete datatypes (more opcodes) and formalization, (e.g. correctness lemmas) is https://github.com/tezos/tezoscoq/tree/new_map_implementation . However as Arthur pointed out the language has changed quite a...

Well it's a matter of personal preferences, I suppose. My own Coq education was done in the ssreflect community and I am more productive using it. Moreover, the `path` library...

The type `int` is mathematically the same as `Z`. For the use we make of it (correctness of factorial), there is certainly the same amount of theory on both sides....

I meant proving properties of smart contracts which involve computations on integers; `mathcomp` has all possible mathematical lemmas you might want about integers, with a systematic, well-thought naming convention. Moreover,...

Yes, I think `tezos.v` is obsolete and the rest is correct.