Mathlib.Util.IncludeStr
source
include_str
A term macro that includes the content of a file, as a string.