| import numpy as np | |
| def _html_repr_helper(contents, index=()): | |
| dims_left = contents.ndim - len(index) | |
| if dims_left == 0: | |
| s = contents[index] | |
| else: | |
| s = ''.join(_html_repr_helper(contents, index + (i,)) for i in range(contents.shape[len(index)])) | |
| return "<div class='numpy-array-ndim-{} numpy-array-ndim-m{}' title='[{}]'>{}</div>".format( |
| 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) |
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)
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
| from functools import wraps | |
| #Create a class to house the methods | |
| class fires(object): | |
| @staticmethod | |
| def whenCalled(event): | |
| e = (lambda s: getattr(s, event)) if type(event) == str else (lambda s: event) | |
| def decorator(f): | |
| """Fires the event before the function executes""" |
| --quick implementation of python's id function. Fails for built in roblox objects | |
| id = function(o) | |
| return type(o) == "table" and o.__id__ or tonumber(tostring(o):sub(-8, -1). 16) | |
| end | |
| class = setmetatable({}, { | |
| __call = function(_, name, implementer) | |
| local cls = {__init__ = function() end, __name__ = name} | |
| local instancemt = {} |
| 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.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 |
| 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 := |
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.valueM[Class](*args, **kwargs) - Match an instance of a specific classM([a, *M._, c]) - Match against [a, *_, c]M([a, *(rest := M._), c]) - Match against [a, *rest, c]