Is there some "pure" function that reads a file before the program is type-checked and returns its contents as a string or something, for example if the file
file.txt has the contents
hello then I could write
example : readFile "file.txt" = "hello" := rfl
The reason I am asking is because I would like to implement a domain-specific language that compiles to a proof of something in Lean. For example if the file has a proof then I could write
example : 2 + 2 = 4 := interpretProof (readFile "file.txt") /- or -/ theorem p : thingProvedBy (readFile "file.txt") := interpretProof (readFile "file.txt") #check p -- p : 2 + 2 = 4
The alternatives that I can think of would be to (a) compile the DSL into Lean code and import it or (b) implement the DSL using the Lean macro system so that it can be written directly in a Lean program.
interpretProofpart of the metaprogram as well for performance. $\endgroup$