Joachim Breitner
Joachim Breitner
The first half, mutual inductive types, are in #4575. Nested inductive types will follow eventually (hence not closing this yet)
Forgot to close this with #4733
> Hmmm, the Mathlib CI isn't happening automatically? My bad. Once https://github.com/leanprover/lean4/pull/4632 is merged your next push might have chance of doing the mathlib thing again.
Putting the assignment `x := 1+1` into the local context before elaborating the tactic seems to be most correct behavior to me, if it can be made to work. The...
Ah, right. I believe we have `nat` there in the first place for two reasons 1. field names may be hashes 2. ordered, unnamed fields, i.e. tuples If the first...
BTW, the size may actually be smaller in some cases. For example, if you have a field name `name` that appears in _n_ types. The leb128-encoding of the 32bit number...
Just another occurrence of this. In https://github.com/dfinity-lab/dfinity/pull/4812 I ran into ``` Public Spec acceptance tests canister lifecycle: FAIL (9.93s) Is running? (3.12s) src/IC/Test/Spec.hs:1091: Candid decoding error: Unexpected variant tag 3099235807...
I wrote that idea down somewhere else a while ago, but probably should be here too: We could include field names in a backward compatible way, by introducing a convention...
Small suggestion, but if you do add something like this, call it `toolchain`, not version. This way there is no confusion about lean4web versions or mathlib versions etc. That said,...
I would push back on heuristics trying to find a “better” project and suddenly using a mathlib project when it originally used a plain lean project. That seems too bad...