Joachim Breitner comments

Results 908 comments of


                                            Joachim Breitner

fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance, no chaining

@DanielFabian , this does successfully build mathlib, and I have a sense that this is a step in the right direction. Do you want to have a final look before...

refactor: IndPredBelow: use `apply_assumption`

@DanielFabian. Here too: It seems that backwards chaining is more powerful than we need here. WDYT of this change, to make it more clear that we don’t expect recursive search...

fix: improve proof search in IndPredBelow

Ok, we now get test failures because the `.brecOn` construction succeeds now (previously it was failing silently), and then the function definitions compilation fails in a way that #4827 is...

fix: improve proof search in IndPredBelow

Obsoleted by #9995

Exporting / importing passive data segments?

> On the other hand, the data container module would probably have to be instantiated once for each memory that wants the data it provides, and I wouldn't necessarily want...

Allow containers 0.7

Thanks, made a revision on hackage an will leave this open until I've updated the code here.

A sketch for stable functions

> Together, these allow identifying any stable function by their "name path" relative to the enclosing actor Is that true? What about shadowing of names inside stable functions. ``` actor...

A sketch for stable functions

Is there convincing prior art for this kind of stuff, or is this exploring a pretty new design space corner?

Support for mutual and nested inductive types as `DecidableEq` instance generator

For mutual, this has been fixed a while ago in #2591. For nested we are now in a good position to have it, with mutual recursion over nested inductives. @arthur-adjedj...

Logspam: [WARNING] System.Taffybar.WindowIcon - Failed to load icon from filepath vscode

I paid a bit more attention, and I get five lines ``` [WARNING] System.Taffybar.WindowIcon - Failed to load icon from filepath vscode [WARNING] System.Taffybar.WindowIcon - Failed to load icon from...