Lean 4 (Meta)programming Cookbook

Marginal Notes🔗

You can add marginal notes that appear in the side margin like: {margin}[Marginal text]. This would give effect as: Marginal notes are great for extra context.