Module Process_file

module Process_file: sig .. end
The full environment built after all typechecking, and transforming

val parse_file : string -> Ast.defs * Ast.lex_skips
type instances = Types.instance list Types.Pfmap.t 
val output : Typed_ast.env ->
Typed_ast.var_avoid_f -> -> string option -> Typed_ast.checked_module list -> unit
val output_alltexdoc : Typed_ast.env ->
Typed_ast.var_avoid_f ->
string -> string -> Typed_ast.checked_module list -> unit
output_alltexdoc produces the latex output for all modules in a single file
val always_replace_files : bool Pervasives.ref
always_replace_files determines whether Lem only updates modified files. If it is set to true, all output files are written, regardless of whether the files existed before. If it is set to false and an output file already exists, the output file is only updated, if its content really changes. For some backends like OCaml, HOL, Isabelle, this is benefitial, since it prevents them from reprocessing these unchanged files.
val only_auxiliary : bool Pervasives.ref
only_auxiliary determines whether Lem generates only auxiliary files
val output_sig : Format.formatter -> Typed_ast.env -> unit