G. Allais
G. Allais
@ice1000 I'd avoid this kind of unnecessarily graphic imagery: you don't know what other contributors' lives have been like and this could ruin their day by invoking horrible memories to...
You'll need a CHANGELOG entry as it's a breaking change for people who are relying on `≤-total`'s reduction behaviour on open terms.
It does work if I make `callGuarded` `public export`. That may very well be the intended behaviour although I would expect to be able to distinguish exporting the definition to...
Based on live sightings, I believe @mjustus got it to work for the REPL in emacs.
They are run, however without any logging so this debugging code is not printed.
Given this type is proof irrelevant, I don't think we should make the exact shape of the proofs part of the module interface.
> PRs are, however, more than welcome. Are they? I don't know that we have the capacity to review opened PRs. e.g. #623
One problem I can see: what should the multiplicity of the as-pattern be when the variable is linear? For zero and unlimited, we can pick zero & unlimited. Otherwise should...
> In all other cases, I need to remember how to type them (this wastes brain space), or I have to copy-paste them (this wastes time). Emacs has a `M-x...
I agree that if you are publishing static material you may want to throw in additional information on how to type some of the symbols. It's not unheard of to...