leanblueprint projects use remark/example environments with labels, \lean{}, and \uses{} (e.g. Sphere-Packing-Lean's SpherePacking structure remark). The native grammar allows only definition|lemma|proposition|theorem|corollary, so the migration maps them to definition with a provenance line. Either add the kinds end-to-end (parser, canvas styling, grammar docs) or document the mapping as the blessed behavior.
🤖 Generated with Claude Code
leanblueprint projects use
remark/exampleenvironments with labels,\lean{}, and\uses{}(e.g. Sphere-Packing-Lean'sSpherePackingstructure remark). The native grammar allows only definition|lemma|proposition|theorem|corollary, so the migration maps them todefinitionwith a provenance line. Either add the kinds end-to-end (parser, canvas styling, grammar docs) or document the mapping as the blessed behavior.🤖 Generated with Claude Code