Up  

Functor Backend.Make


module Make: 
functor (C : sig
val avoid : Typed_ast.var_avoid_f
val env : Typed_ast.env
val dir : string

the directory the output will be stored. This is important for setting relative paths to import other modules




end) -> sig .. end
The various backends that generate text from typed asts
Parameters:
C : sig val avoid : Typed_ast.var_avoid_f;; val env : Typed_ast.env;; val dir : string (** the directory the output will be stored. This is important for setting relative paths to import other modules *) end 
val ident_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
val lem_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
val hol_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t option
val ocaml_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t option
val isa_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t option
val isa_header_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
val coq_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t
val tex_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
val tex_inc_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t
val html_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
val ident_exp : Typed_ast.exp -> Ulib.Text.t
val ident_pat : Typed_ast.pat -> Ulib.Text.t
val ident_src_t : Types.src_t -> Ulib.Text.t
val ident_typ : Types.t -> Ulib.Text.t
val ident_def : Typed_ast.def -> Ulib.Text.t