Rob23oba
Rob23oba
size_t and void are currently not types supported by porffor, you might be able to use u64 and undefined instead
Well, there's not much optimization currently since that's not really the focus right now. In the future such code should compile again to reasonable sizes.
Also, `porf -e "console.count"` (or countReset / time / timeLog / timeEnd) crashes with `TypeError: Cannot read properties of undefined (reading 'ind')` in assemble.js where it generates the data section
Also adds `--size-log` and `--size-log-count`: - `--size-log`: Show the functions with the highest amount of instructions - `--size-log-count`: How many instructions to show for `--size-log`
Yeah, I just had them in the same branch more or less accidentally.
Okay, this was slightly annoying to do but I now re-organized this branch to only contain bigint stuff
Yeah, I've noticed that one before. I believe that is because a 64-bit random number generator is used but only 32-bit seeds. Another problem is that after compilation, the series...
Here's another idea, inspired by how inductive predicate `brecOn` works now: ```lean-4 def Nat.brec.below.{u} {motive : Nat → Sort u} (F_1 : (t : Nat) → @Nat.below motive t →...
The idea is to create an application of `F_1` on the outer level instead of merely burying it in the recursor application. So basically similar to defining `brecOn` as `f...
> And do the desired definitional equalities still hold, e.g. > > theorem Nat.add2_eq1 (a b : Nat) : Nat.add2 (a.succ) b = (a.add2 b).succ := rfl Yes (not this...