G. Allais comments

Results 513 comments of


                                            G. Allais

Making `IStateT` a record to prevent its unfolding and increase readability?

Nevermind: the instance I had in scope was a tad too specific and didn't match the problem at hand. Wrapping `IStateT` in a record lead to clearer types in the...

Making `IStateT` a record to prevent its unfolding and increase readability?

Edit: nevermind, `RawMonadState` opens `RawMonad` already so then there are two binds in scope (twice the same one...) and Agda gets confused.

Formalize `Prefix`, `Suffix` and `Infix` as relations on Lists

Something to think about: Suffix could be generalised to ```agda module _ (R : REL (List A) (List B) r) where data Suffix : REL (List A) (List B) (a...

Adapt to reflection interface changes

I'm not a fan of just having a `Bool` there. Can we throw in a more informative sum type?

Adapt to reflection interface changes

I don't mean necessarily more information but a type with informative constructor names.

Poor type checking performance with many subcommands

This may be an upstream problem if we're breaking sharing and recomputing a lot of the same checks.

Define `strictify` function at each base type, plus evident property

Is this redundant with [`Function.Strict`](http://agda.github.io/agda-stdlib/v2.1/Function.Strict.html)? I also expect some of these will be optimised away by MAlonzo.

Evaluation of partial functions during conversion

You are explicitly trying to evaluate a partial function at the type level. It's bound to end badly. ``` EvalTy (ProdK k1 k2) p = (EvalTy k1 (Fst p), EvalTy...

Redefine `Algebra.Consequences.Setoid.wlog`

I think we should find a use case of this function before refactoring it! IME it's utterly useless and I always had to resort to the more general `Binary.Consequences` definition....

Adds unary disjoint relation

I've opened https://github.com/agda/agda/pull/7791/files to add the relevant unicode symbols