G. Allais
G. Allais
Oops, did not see zoe's original answer. I don't think you can disable the optimisation atm.
I already do something somewhat similar in `base`: instead of deriving functions directly by analysing the type, I start by computing a view of it that is known to be...
We may end up opening other issues if we find bugs but for now, given how far we've come, I consider this solved: https://github.com/pigworker/Syrup/pull/14#issuecomment-2191354245
Can you not get the normalised result by prefixing with `C-u C-u`? It may better not to do arbitrary normalisation unless the user requests it explicitly.
``` Id : Type -> Type Id a = a ``` means `ω Id : Type -> Type`. But from the typing rule you're showing, you seem to suggest it's...
In a homework we used a REWRITE pragma to add a typechecking-time computational behaviour to an (abstract) function defined in terms of low-level primitives. Unfolding the abstract definition means the...
It's in the icebox meaning no one has plans to work on this.
They're there but commented out in the source. And the empty section header is "Fill combi**an**tors".
I deleted my original message because, even though `_+_` is indeed defined in one of the builtin files and that's the definition used during proofs, there is also black magic...
> The problem with local-only functions is that it's hard to prove things about them. You perhaps mean something else but if the issue is that you cannot refer to...