eric-wieser

import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

set_option pp.proofs.withType false

variable {R M} [CommRing R] [Invertible (2 : R)] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M)

abbrev ExteriorAlgebra.rMultivector (r : ℕ) : Submodule R (ExteriorAlgebra R M) :=
  (LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] _) ^ r)

eric-wieser

A tool to estimate "meaningful" edges betweeen typeclass instances in mathlib. Click the raw button on the SVG to zoom in on the graph.

You can regenerate the separate graphs with

lean --run instance_graph.lean > gviz/out.gviz
ccomps gviz/out.gviz "-zX#0" | dot | gvpack -g -m48 -Glabel=\"\" | neato -n2 -Tsvg > gviz/out-large.svg
ccomps gviz/out.gviz "-zX#1-" | dot | gvpack -g -m48 -Glabel=\"\" | neato -n2 -Tsvg > gviz/out-small.svg

(you might need to sudo apt install graphviz)

eric-wieser

The "Editorial manager" software used by springer journals such as Advances in Applied Clifford Algebra behaves poorly on latex files that include \usepackage{minted}. When provided with such a file, the software starts a build, and reports back 15 minutes later with the output "Error" and nothing else.

Some more details are given in the blog post "The pain with submitting LaTeX to a journal".

I tracked down the issue to \RequirePackage{ifplatform} failing. Since we know that the platform is windows and does not support shellescape, we can insert a shim for this package with the following ifplatform.sty:

\ProvidesPackage{ifplatform}
  [2007/11/18 v0.2  Testing for the operating system]
\newif\ifshellescape

eric-wieser

import data.quot
import tactic


variables {α : Type*} (P : α → Prop)

/-- A choosable instance is like decidable, but over `Type` instead of `Prop` -/
@[class] def choosable (α : Type*) := psum α (α → false)

/-- inhabited types are always choosable -/

eric-wieser

import data.dfinsupp
import tactic

universes u v w

variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables (β : ii → jj → Type w) [Π i j, decidable_eq (β i j)]
variables [Π i j, has_zero (β i j)] 

def to_fun (x : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j :=

eric-wieser

import data.finsupp

namespace finsupp.eric

#check finset.sigma


universes u v w
def bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α → finset β) : finset (α × β)
  := (sa.sigma fb).map (equiv.sigma_equiv_prod _ _).to_embedding

eric-wieser

This shows how the walrus operator (:=) can be exploited to write pattern matching without needing PEP622 at all.

Supported patterns:

• M._ - wildcard which matches anything
• (x := M._) - bound match, result is stored in x.value
• M[Class](*args, **kwargs) - Match an instance of a specific class
• M([a, *M._, c]) - Match against [a, *_, c]
• M([a, *(rest := M._), c]) - Match against [a, *rest, c]

eric-wieser

Partially-structured thoughts in response to https://numpy.org/neps/nep-0041-improved-dtype-support.html

---

Quoting @teoliphant from the mailing list

But, this is the right way to connect the data type system with the rest of Python typing.  NumPy's current dtypes are currently analogous to Python 1's user-defined classes.  In Python 1 all user-defined classes were instances of a single Class Type at the C-level, just like currently all NumPy dtypes are instances of a single Dtype "Type" in Python.

I'm not really following here. In python 3.x, all user-defined classes are instances of type at the python level. At the C level, almost all classes have the layout of either PyTypeObject (note that while the layout PyHeapTypeObject is sometimes used, this layout is not a different python type!).

eric-wieser

An attempt to emulate C++ templates in python, complete with non-type template parameters.

eric-wieser

#include <utility>

template<typename T, typename U>
class out_arg;

/** Use in a parameter list for an output argument. Can only be assigned to. */
template<typename T>
class out_param {
private:
    T& val;