Include contents of a file as string

Stream: general

[Greg Shuflin]

Is there a way to include the contents of a file on disk as a string at compile time?

[Kyle Miller]

Yes, see docs#Lean.includeStr

(Note that mathlib contains its own copy of this that somebody ought to delete, otherwise you get an ambiguity error.)

[Kim Morrison]

#19828