Division Theorem. For every natural number `x` and positive natural
number `n`, there is a unique decomposition:
`x = q*n + r`
with `q`,`r` natural and `r` < `n`.
`q` is the quotient when dividing `x` by `n`
`r` is the remainder when dividing `x` by `n`.
This commit adds a proof for this fact, in case
we want to reason about modular arithmetic (for example, when dealing
with binary representations). A future, more systematic, development could
perhaps follow: @clayrat 's (idris1) port of Coq's binary arithmetics:
https://github.com/sbp/idris-bi/blob/master/src/Data/Bin/DivMod.idrhttps://github.com/sbp/idris-bi/blob/master/src/Data/Biz/DivMod.idrhttps://github.com/sbp/idris-bi/blob/master/src/Data/BizMod2/DivMod.idr
In the process, it bulks up the stdlib with:
+ a generic PreorderReasoning module for arbitrary preorders,
analogous for the equational reasoning module
+ some missing facts about Nat operations.
+ Refactor some Nat order properties using a 'reflect' function
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
This mirrors the (>>) found in Haskell, which is the same as (>>=), except the
second computation (on the right hand side) takes no arguments, and the result
of the first computation is discarded. This is a trivial implementation written
in terms of (>>=).
The Network.Socket.Data code previously used hardcoded constants manually read
from auto-generated C source code, however these constants are specific to
Linux. The original code looked like this:
export
ToCode SocketFamily where
-- Don't know how to read a constant value from C code in idris2...
-- gotta to hardcode those for now
toCode AF_UNSPEC = 0 -- unsafePerformIO (cMacro "#AF_UNSPEC" Int)
toCode AF_UNIX = 1
toCode AF_INET = 2
toCode AF_INET6 = 10
The AF_INET6 constant is correct on my Debian 10 laptop:
molly on flywheel ~> grep -rE '^#define AF_INET6' /usr/include
/usr/include/x86_64-linux-gnu/bits/socket.h:#define AF_INET6 PF_INET6
molly on flywheel ~> grep -rE '^#define PF_INET6' /usr/include
/usr/include/x86_64-linux-gnu/bits/socket.h:#define PF_INET6 10 /* IP version 6. */
However, this is not the case on an OpenBSD machine:
spanner# grep -rE '^#define[[:space:]]+AF_INET6' /usr/include
/usr/include/sys/socket.h:#define AF_INET6 24 /* IPv6 */
This commit adds accessor functions to the C runtime support library for
retrieving the values of these macros as they appear in the system libc header
files, which can then be invoked using the normal C FFI machinery.
Things like (,) () aren't straightforward IVar's but are IAlternative's
which present options about how the term should resolve. [| |] was not
accounting for this.
useful items for applying multiple predicates, e.g.
sortBy (comparing length <+> compare)
To sort some lists elements by length and then lexographically
