Jesper Cockx

I guess without any other primitives but `SSet` the answer is no. However, one could for example have a univalent equality in `Set` and a strict equality in `SSet`, in...

The reason why CoverageNoExactSplit is an ErrorWarning instead of a regular Warning is because it was originally only used when the user enabled `--exact-split` explicitly, in which case it makes...

For reference, here's the current definition of `monadT` for `Maybe`: ```agda ------------------------------------------------------------------------ -- Maybe monad transformer monadT : ∀ {f} → RawMonadT {f} (_∘′ Maybe) monadT M = record {...

There's a sidenote about literals for natural numbers at https://github.com/jespercockx/agda-lecture-notes/blob/f3c8529504684a275b3cac569bea21b0476c1d3f/agda.lagda.tex#L385-L395, if you include this code then the example should work!

One of the main points of `runSpeculative` is precisely the ability to clean up fresh metavariables from the state, so if we keep them around then we would need some...

Here is the motivating use case: https://github.com/jespercockx/ataca/blob/master/src/Ataca/Core.agda#L72-L78 A boolean would not be enough here, but what would work would be to change `runSpeculative` to have type `TC (Maybe A) ->...

Are you sure that the new method has the same behaviour under POSIX and Windows? As long as that's still the case, I'm fine with it.

The problem here is that Agda gets confused about the type of the `★` argument to `G` in the rule `G2`: `★` is a constructor so Agda expects its type...

Would this mean that all variables in a let-binding get lambda-lifted? In that case I do not think this is a good idea.

Yes, but then that should be done *before* we unify `let` and `where`.