Sebastian Ullrich
09a5b34931
feat: make private the default in module ( #9044 )
...
This PR adjusts the experimental module system to make `private` the
default visibility modifier in `module`s, introducing `public` as a new
modifier instead. `public section` can be used to revert the default for
an entire section, though this is more intended to ease gradual adoption
of the new semantics such as in `Init` (and soon `Std`) where they
should be replaced by a future decl-by-decl re-review of visibilities.
2025-06-28 16:30:53 +00:00
Markus Himmel
781c94f2cf
chore: test that there are no orphaned modules ( #8082 )
...
This PR adds a test that makes sure that there are no orphaned modules.
2025-04-24 11:55:07 +00:00
Sebastian Ullrich
7feb583b9e
feat: enable experimental module system in Init ( #8047 )
2025-04-23 17:21:33 +00:00
Kim Morrison
fdc62faa0f
feat: reproduce Array.Perm API for Vector.Perm ( #7994 )
...
This PR reproduces the `Array.Perm` API for `Vector`. Both are still
significantly less developed than the API for `List.Perm`.
2025-04-17 02:39:48 +00:00
Kim Morrison
88664e4a99
feat: complete aligning List/Array/Vector.finRange ( #7106 )
...
This PR completes the alignment of `List/Array/Vector.finRange` lemmas.
2025-02-17 06:11:43 +00:00
Kim Morrison
9d1fb9f4fa
feat: align Array/Vector.extract lemmas with List ( #7105 )
...
This PR completes aligning `Array/Vector.extract` lemmas with the lemmas
for `List.take` and `List.drop`.
2025-02-17 04:56:04 +00:00
Kim Morrison
2385abc282
feat: align List/Array/Vector.insertIdx lemmas ( #6948 )
...
This PR completes the alignment of `List/Array/Vectors` lemmas for
`insertIdx`.
2025-02-04 12:23:27 +00:00
Kim Morrison
6c2573fc38
feat: alignment of lemmas about monadic functions on List/Array/Vector ( #6883 )
...
This PR completes the alignment of lemmas about monadic functions on
`List/Array/Vector`. Amongst other changes, we change the simp normal
form from `List.forM` to `ForM.forM`, and correct the definition of
`List.flatMapM`, which previously was returning results in the incorrect
order. There remain many gaps in the verification lemmas for monadic
functions; this PR only makes the lemmas uniform across
`List/Array/Vector`.
2025-01-31 07:25:24 +00:00
Kim Morrison
40eefb1df6
feat: alignment of List/Array/Vector lemmas about range, range', zipIdx ( #6878 )
...
This PR completes alignments of `List/Array/Vector` lemmas about
`range`, `range'`, and `zipIdx`.
2025-01-31 00:06:51 +00:00
Kim Morrison
5bd75695f4
feat: align List/Array/Vector eraseP/erase/eraseIdx lemmas ( #6868 )
...
This PR completes the alignment across `List/Array/Vector` of lemmas
about the `eraseP/erase/eraseIdx` operations.
2025-01-30 12:29:55 +00:00
Kim Morrison
bc234f9f8d
feat: align List/Array/Vector.zip/zipWith/zipWithAll/unzip ( #6840 )
...
This PR completes the alignment of
`List/Array/Vector.zip/zipWith/zipWithAll/unzip` lemmas.
2025-01-29 07:58:17 +00:00
Kim Morrison
e05131122b
feat: finish aligning List/Array/Vector.ofFn lemmas ( #6838 )
...
This PR completes aligning the (limited) verification API for
`List/Array/Vector.ofFn`.
2025-01-29 04:53:33 +00:00
Kim Morrison
84311122ac
feat: align List/Array/Vector lemmas for isEqv and == ( #6831 )
...
This PR completes the alignment of `List/Array/Vector` lemmas about
`isEqv` and `==`.
2025-01-29 03:12:02 +00:00
Kim Morrison
22117f21e3
feat: align List/Array/Vector.count theorems ( #6712 )
...
This PR aligns `List`/`Array`/`Vector` theorems for `countP` and
`count`.
2025-01-20 10:20:16 +00:00
Kim Morrison
ac6a29ee83
feat: complete alignment of {List,Array,Vector}.{mapIdx,mapFinIdx} ( #6701 )
...
This PR completes aligning `mapIdx` and `mapFinIdx` across
`List/Array/Vector`.
2025-01-20 04:06:37 +00:00
Kim Morrison
c3948cba24
feat: upstream definition of Vector from Batteries ( #6197 )
...
This PR upstreams the definition of `Vector` from Batteries, along with
the basic functions.
2024-11-24 23:01:32 +00:00
