Reed Mullanix comments

Results 153 comments of


                                            Reed Mullanix

Problem with `Tactic.MonoidSolver`

Looks like the monoid solver isn't normalizing before doing reflection, so it thinks `x ∷ (ys ++ zs)` has to be treated like a opaque expression. This could be fixed...

Some stuff im working on

Realisation seems fine for the free objects. Not sure how I feel about れ or さ though; seems like it could make things difficult to read. As for T-spans, be...

Trivial solution set for Adjoint functor theorem

I am a bit suspicious of the size of completeness required; it seems like this would run afoul of https://ncatlab.org/nlab/show/complete+small+category

Trivial solution set for Adjoint functor theorem

See https://mathoverflow.net/questions/438333/small-complete-categories-in-hottlem/438568#438568

Trivial solution set for Adjoint functor theorem

The proof is fine, it’s just that the hypothesis are too strong to make it something you can actually use.

Port defadvice to define-advice

No, `define-advice` has been available since Emacs 25.1.

Port defadvice to define-advice

Closing as https://github.com/abo-abo/hydra/commit/59a2a45a35027948476d1d7751b0f0215b1e61aa removed the problematic advice.

Improve module checkpointing performance

Thanks! Unfortunately the CI failure is indicative of a real bug in my code, so I can't load the stdlib right now 😁 Going to bite the bullet and do...

Improve module checkpointing performance

There's also some other nice low-hanging fruit in this area of the code. Using a `Map` for checkpoints in TCEnv is seems somewhat suboptimal: `IntMap` should be a drop-in replacement....

Improve module checkpointing performance

Looks like the bug was that something reset the `TCState` while inside of a `checkpoint` to a state that had no module checkpoints. I've made `checkpoint` more robust to state...