Lean 4 (Meta)programming Cookbook

Errors and Warnings🔗

Expected errors must be explicitly marked with +error. If the error message does not match exactly, the documentation build may fail.