🕴️

Anne Baanen Vierkantor

🕴️

Vierkantor / lake build --no-build -v Mathlib

Created July 30, 2025 13:29

This file has been truncated, but you can view the full file.

	✔ [0/859] Ran mathlib:extraDep
	✔ [1/859] Replayed Mathlib.Tactic.Linter.DirectoryDependency
	✔ [2/859] Replayed Mathlib.Tactic.Linter.Header
	✔ [3/859] Replayed Mathlib.Tactic.Linter.CommandStart
	✔ [4/859] Replayed Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
	✔ [5/859] Replayed Mathlib.Tactic.Linter.DocPrime
	✔ [6/859] Replayed Mathlib.Tactic.Linter.DocString
	✔ [7/859] Replayed Mathlib.Tactic.Linter.GlobalAttributeIn
	✔ [8/859] Replayed Mathlib.Tactic.Linter.HashCommandLinter
	✔ [9/859] Replayed Mathlib.Tactic.Linter.FlexibleLinter

Vierkantor / get-top-level-imports.lean

Last active March 14, 2025 16:18

transitive top-level imports

	import Mathlib

	open Lean Elab Command

	/-- Get the top-level directory for this name.

	For example: (`Mathlib.Data.Nat.Init).topLevel = `Mathlib.Data.
	-/
	partial def Lean.Name.topLevel (n : Name) (length := 2) : Name :=
	if n.getNumParts <= length then n else n.getPrefix.topLevel (length := length)

Vierkantor / invertible.lean

Last active April 23, 2020 12:38

invertible.lean (WIP)

	import tactic

	universes u

	variables {α : Type u}

	/-- `invertible a` gives a two-sided multiplicative inverse of `a` -/
	class invertible [has_mul α] [has_one α] (a : α) : Type u :=
	(inv_of : α) (inv_of_mul_self : inv_of * a = 1) (mul_inv_of_self : a * inv_of = 1)

Vierkantor / gist:3693994

Created September 10, 2012 21:26

Buildcraft Dutch translation

	# nl_NL
	# Translated by Raeon

	gui.building.resources=Bouwmaterialen
	gui.del=Del
	gui.filling.resources=Opvulmaterialen
	gui.inventory=Inventaris
	gui.lock=Sluiten
	gui.needed=Nodig
	gui.unlock=Openen