András Kovács

To be concrete about the development history of the "efficient unfolding control" feature, I first included it in the old smalltt branch in a more complicated way, then ollef used...

There are small examples here: - https://github.com/AndrasKovacs/smalltt/blob/989b020309686e04374f1ab7844f468386d2eb2f/bench/asymptotics.stt - https://github.com/AndrasKovacs/smalltt/blob/989b020309686e04374f1ab7844f468386d2eb2f/bench/asymptotics.agda These are highly synthetic though. The current smalltt implementation preserves all top-level unfoldings in meta solutions. In real code, this can...

@JasonGross testing `native_compute` with expressions like `(const n10 t8M)` ran in about 70ms (perhaps there's some caching going on in aux files?), which suggests that compilation does not significantly change...

Some pros and cons: #### Eliminators (induction principles). + Formally nice. + Relatively simple to implement. + Can be inconvenient. E.g. injectivity and disjointness of constructors is not built-in and...

To me, the distinguishing feature of miniTT case splits is the lack of nesting and argument permutation, when compared to Agda patterns. So I view it as a minimal version...

> pattern matching lambdas (too complicated?) MiniTT's splitting is via pattern matching lambdas. They're simpler IMO than Coq-style matching, where the matching is not tied to a lambda. > the...

> How do you define pattern matching? I tend to use "pattern matching" for anything which is not eliminators. > some fundamental issue going on here As an example, [this...

Do you know perhaps how to check for architectures? I searched just now and didn't find out. It makes sense to do it, but I'd consider it very low priority....

Thanks!

Thanks, I was silly to not use `ulimit` when I already used it for F#. However, setting `OCAMLRUNPARAM` seems to have no effect at all. Would this only work for...