Module Process_file

module Process_file: sig .. end

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 ->
       Target.target -> 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