Eric Wieser

feat: notation for Euclidean space

4

This adds `!ₑ[1, 2, 3]` notation for `(WithLp.equiv 2 (∀ _ : Fin 3, _)).symm ![1, 2, 3]`, which is a term of type `EuclideanSpace 𝕜 (Fin 3)`. This reduces...

**Description:** The old matcher only worked if the error was raised with `raise Exception('single quotes')`. This represents a miniscule fraction of errors; for instance, `l[37]` on a short list `l`...

fix: add missing `initHeartbeats`

6

In only one case a `Core.Context` is created from within CoreM, and we inherit from the parent Context the `initHeartbeats`. Otherwise, we get the current heartbeats from IO. It's not...

Syntax-highlight comments in verso code

1

It would be great if a dedicate `span` tag was placed around `--` and `/-` comments within a lean code snippet. In https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html, I hacked around this with ```css .hl.lean...

This will require a mathlib patch

Remove the space from Lean 4

1

This makes `lean4` work as a markdown block language instead of `lean-4`. ## Description This change is consistent with how Pygments-based highlighters demarcate Lean 4. I estimate that exactly no...

Add methods from the builtin float types to the numpy floating point types

8

Asking for methods that exist on builtin float types but not numpy types gives: ```python >>> set(dir(float)) - set(dir(np.float32)) {'__getformat__', '__getnewargs__', '__setformat__', '__trunc__', 'as_integer_ratio', 'fromhex', 'hex', 'is_integer'} ``` Filtering these...

BUG: Integer overflow warning applies to scalars but not arrays

9

Simple demo: ```python In [1]: np.uint8(0) - np.uint8(1) RuntimeWarning: overflow encountered in ubyte_scalars Out[1]: 255 In [2]: np.uint8(0)[...] - np.uint8(1)[...] Out[2]: 255 ``` Should we even warn at all for...

compare_buffer_info does not consider <i and i equal on a little-endian machine

1

The `compare_buffer_info` template will reject buffer formats of `