~cypheon/Idris2

b61ccaf3 — Johann Rudloff 14 days ago rapid
Allow access to raw (post-CSE) `CDef`s via CompileData
8010e6cf — Johann Rudloff 14 days ago
Export some useful functions related to `Names` handling
45fd479f — Johann Rudloff 16 days ago
Add implementation `Weaken CConstAlt`
55ce9477 — Johann Rudloff a month ago main
Merge remote-tracking branch 'origin/main'
7a863556 — Guillaume Allais a month ago
[ fix ] missing Show implementation
fdbd858d — G. Allais a month ago
[ refactoring ] expose some internals needed by Katla (#2480)

71351a6c — Zoe Stafford a month ago
Merge pull request #2476 from Z-snails/bits64-popcount

Fix `FiniteBits` for `Bits64`
8a0d75dc — Zoe Stafford a month ago
Fix `FiniteBits` for `Bits64`
72f0a2ab — Denis Buzdalov a month ago
[ re #950 ] Remove redunant legacy data definition

`Given` with `Always` from Idris 1 library are completely overridden by
`IsYes` and `ItIsYes` respectively, which have a more common naming.
This, however, may break some very old code (fixed by a trivial rename).
d037b39e — Denis Buzdalov a month ago
[ base ] Add injectivity proof for `Yes` and `No`
bf87b623 — Joel Berkeley a month ago
add `scanr`; `scanr1`; `unsnoc` for `Vect` (#2471)

* add `scanr` and `scanr1` for `Vect`

* add tests

* tests

* docstring

* typos

* add unsnoc

* simplify unsnoc

* docstring

* typos
7c784dd8 — Guillaume Allais a month ago
[ fix ] missing rigs in doc type signatures
a1e762a2 — Guillaume Allais a month ago
[ re #1282 ] Documenting my understanding

I don't think it's worth fixing as the new core and its first class
case blocks should hopefully solve this issue.
f80fc184 — G. Allais a month ago
[ new ] `:exec` for RefC (#2466)

fix a case typo in document
466e14a1 — Denis Buzdalov 2 months ago
[ base ] Add a dependent funext function to the `FunExt` interface
db13a35b — Jesse Nava a month ago
[ fix ] Ensure casting from String to Double results in floating numbers on scheme backends
76184915 — György Kurucz a month ago
[ refactor ] Use switch statement in `extractInt` in the RefC runtime

Modern compilers should be smart enough regardless and generate
efficient code for the sequence of ifs, this is really just a syntax
change to make the code shorter.
7a5f63ea — György Kurucz a month ago
[ fix ] Add missing cases for BITS types in `extractInt`

e79e4277 ("[ fix ] Make Bits types use int switch statement in RefC")
made the RefC backend generate code calling `extractInt` with Bits
types, bit did not add the extra cases to `extractInt`. This commit adds
the missing cases.

Fixes #2452
a05f091a — György Kurucz a month ago
[ refactor ] Format support/refc/runtime.c with `clang-format`
Next