Paul Reichert

Tweak denormalizeBindingsList performance

2

The query engine often redundantly fetches same objects from the lexicon in denormalizeBindings(List). Using a lazy cache for the already fetched items reduces the request time significantly; an exemplar query...

Fix issue #127.

SELECT * WHERE { } should return one result

1

`SELECT * WHERE { }` doesn't match any result. Normally, it should: https://www.w3.org/TR/rdf-sparql-query/#emptyGroupPattern This simple case really doesn't bother me but in consequence, `SELECT * WHERE { { ?s ?p...

feat: target of final functor is connected iff source is connected

3

This PR is part of the effort to prove the Freyd-Mitchell embedding theorem. --- [](https://gitpod.io/from-referrer/)

The branch on which I try migrating the old ranges to the new ones.

refactor: migrate all usages of old slice notation

7

This PR replaces all usages of `[:]` slice notation in `src` with the new `[...]` notation.

feat: introduce slices

3

This PR introduces polymorphic slices in their most basic form. They come with a notation similar to the new range notation. `Subarray` is now also a slice and can produce...

feat: `MonadAttach`

3

This PR adds the new operation `MonadAttach.attach` that attaches a proof that a postcondition holds to the return value of a monadic operation. Most non-CPS monads in the standard library...

refactor: move Std.Range to Std.Legacy.Range

2

This PR renames the namespace `Std.Range` to `Std.Legacy.Range`. Instead of using `Std.Range` and `[a:b]` notation, the new range type `Std.Rco` and its corresponding `a...b` notation should be used. There are...

### Prerequisites * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or...