mechvel
mechvel
Maybe join it with wishes for Nat.Properties ? ("Big wish list for Data.Nat(Integer).Properties"). For example, I had several wishes for Nat.Properties: I am not sure, may be some of them...
May be, this one is useful: ``` pred-n
The matter is also in that `*-cancel...nonZero` does rely on `suc`. Many domains have not any sensible `suc`.
But the generic `_∣_` is already defined in `lib-1.7` in `Algebra.Definitions.RawMagma` as ``` x ∣ʳ y = ∃ λ q → (q ∙ x) ≈ y -- Gen-1.7 _∣_ =...
Strangely, this editor cancels many of underscores that I set in the code. Let me try to copy-paste the underscore from the first line: _≈_
How to enter here the underscore symbol?
On Sun, 2018-03-18 at 08:06 -0700, MatthewDaggitt wrote: > Hmm I can envisage a use case for such a proof. Not sure about the > name Respects₂gen though. My alternative...
> The Algebra.Operations folder is entirely deprecated. This is nice. > Could you elaborate on what you mean by Foo-reexport? We don't use - in names nor lowercase letters. For...
The generic ``IsNonzero : Pred Carrier _`` can be defined only as ``_≉ 0#``. Because in an arbitrary semiring it does not hold ``∀ x → 1 + x ≉...
I have committed this PR. I hope that it does not override the PR of Binary.DivMod. I have entered ``https://github.com/agda/agda-stdlib`` and clicked at Fork. Then I created the folder ``foo/NonzeroPR/``...