1 of 8

Tips and tricks for beginners

using Mathlib/Lean

2 of 8

Plan

​

[some slides here are just placeholders for interactive lean demonstrations]

3 of 8

Fun with casting

4 of 8

Nat.digits

  • order of arguments (base first!)
  • order or digits (little endian!)

5 of 8

Fun with ranges

6 of 8

Inspecting types

  • #check and #eval
  • use “@” to access implicit arguments
  • make sure to have necessary import (can always minimize with #min_imports)

​

7 of 8

Not wrong, but unidiomatic

  • a > b and a ≥ b ⇒ use b < a and b ≤ a instead
  • 0 ≠ a ⇒ use a ≠ 0 instead
  • Fin 7 versus ZMod 7 ⇒ use what you really need
  • a % d = 0 ⇒ use d ∣ a
  • ℝ≥0 and ℕ+: not as many theorems as we have for ℝ and ℕ.
  • ​

8 of 8

Searching