Skip to content

Instantly share code, notes, and snippets.

View eric-wieser's full-sized avatar

Eric Wieser eric-wieser

View GitHub Profile
@eric-wieser
eric-wieser / GeometricGrades.lean
Created November 21, 2023 13:28
Grade selection with Mathlib
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
eric-wieser / Instance graph.md
Last active August 19, 2023 20:53
Mathlib instance hierarchy

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
eric-wieser / minted-editorial-manager.md
Last active November 10, 2022 04:51
Getting `minted` to work in Editorial Manager

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
eric-wieser / choosable.lean
Created February 3, 2021 16:59
Choice without the axiom of choice
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 -/
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
eric-wieser / finsupp_prod_equiv.lean
Last active July 25, 2020 09:41
An alternative formulation of finsupp.finsupp_prod_equiv
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
eric-wieser / README.md
Last active June 24, 2020 16:57
Pattern matching without PEP 622

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]

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
eric-wieser / README.md
Created November 15, 2019 16:04
C++-style templated types for Python

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

@eric-wieser
eric-wieser / out_params.hpp
Created April 24, 2019 07:44
Output parameters with implicit casting
#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;