aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Revert "Remove a spurious case now correclty rules out by the plugins"Tom Smeding3 days
| | | | | | | This reverts commit 069ac5b0bcf52b8b5414261106e82ef0eb8a582e. The plugins are unsound: https://github.com/clash-lang/ghc-typelits-natnormalise/issues/105
* Remove a spurious case now correclty rules out by the pluginsMikolaj Konarski4 days
|
* Tune redundant cases for no-warnings on GHC 9.12Tom Smeding2025-10-02
|
* Compatibility with GHC 9.6Tom Smeding2025-10-02
|
* Port to ghc-typelits-natnormalise-0.8.1 that is much overhauledport-to-natnormalise-0.8.1Mikolaj Konarski2025-10-02
| | | | and probably more sound than earlier versions.
* Tweak shape ZipWith definitions slightlyMikolaj Konarski2025-07-13
|
* Cross-package doc links are half-broken, let's notTom Smeding2025-06-30
|
* Fix rerank docsTom Smeding2025-06-30
|
* Apply a small fraction of hlint hintsMikolaj Konarski2025-06-30
|
* Permutations: withKnownPermTom Smeding2025-06-29
|
* Add existential conversions to ShSTom Smeding2025-06-29
|
* More shape/index conversion functionsTom Smeding2025-06-29
|
* Flip some index/shape-related functionsTom Smeding2025-06-29
| | | | | This ensures that the argument order consistently puts the main thing being operated on at the end, and supporting singletons at the start.
* Improve Conversion haddocksTom Smeding2025-06-29
|
* CleanupTom Smeding2025-06-29
|
* Tweak haddocs and comments slightlyMikolaj Konarski2025-06-26
|
* Add instance TestEquality PermMikolaj Konarski2025-06-19
|
* Rename Castable to ConversionTom Smeding2025-06-09
|
* Derive instance Show (Castable a b)Mikolaj Konarski2025-06-06
|
* Describe Castable philosophyTom Smeding2025-06-04
|
* Add CastZip and CastUnzipTom Smeding2025-06-04
|
* Add shape checking to [rms]zipTom Smeding2025-06-04
|
* Fix up and update Trace.hsTom Smeding2025-06-04
|
* Reorganise and clean up {from,to}List functionsTom Smeding2025-06-04
|
* Add ssxDropSSX and ssxDropSh, analogous to the shx* versionsTom Smeding2025-06-03
|
* Add CastNest and CastUnnestTom Smeding2025-06-03
|
* Remove unnecessary LANGUAGE pragmaTom Smeding2025-06-02
|
* Make MapJust injectiveTom Smeding2025-06-02
|
* Simplify and expand CastableTom Smeding2025-06-02
|
* Run stylish-haskellMikolaj Konarski2025-05-17
|
* Nested.hs: Fix typo in doc commentTom Smeding2025-05-17
|
* Nested.hs: import and export orderingTom Smeding2025-05-17
|
* Update doc comments in LemmasTom Smeding2025-05-17
|
* Move shape conversion ops to Data.Array.Nested.ConvertMikolaj Konarski2025-05-17
|
* Move code around in Data.Array.Nested.ConvertMikolaj Konarski2025-05-17
|
* Merge both Lemmas modulesMikolaj Konarski2025-05-17
|
* Eliminate the dependency cycle of Lemmas modulesMikolaj Konarski2025-05-17
|
* Move modules Permutation and TypesMikolaj Konarski2025-05-16
|
* Generalize some shape conversion functionsMikolaj Konarski2025-05-16
|
* Revert "Remove the KnownNat constraint from (:5509)"Tom Smeding2025-05-16
| | | | | | | This reverts commit 8890526cac9e6c4d5583d00fce55f32ba613cf31. Removing a _provided_ KnownNat constraint if we cannot remove the actual Nat information from the data type is rather pointless.
* Shape/index function renameTom Smeding2025-05-16
|
* default-show-instances flagTom Smeding2025-05-16
|
* Remove the KnownNat constraint from (:5509)Mikolaj Konarski2025-05-16
|
* Explicit re-exports of Base membersTom Smeding2025-05-16
| | | | | This is to ensure that haddock doesn't insert a module reference, but displays the members of the Base module inline.
* Flip arguments of mcastToShaped for consistencyTom Smeding2025-05-16
|
* Convert: Export list; simplify some functions with castCastableTom Smeding2025-05-16
|
* Move casts to DAN.Convert; split Ranked/Shaped types into .BaseTom Smeding2025-05-15
|
* Make mcast available in CastableTom Smeding2025-05-15
|
* mcastSafe was unsound; it's now goneTom Smeding2025-05-15
|
* Simplify lemRankAppTom Smeding2025-05-15
|
generated by cgit v1.2.3-70-g09d2 (git 2.51.0) at 2025-10-24 17:32:51 +0200