Coq (hax-engine.Coq

Parameters

module Lib : Library

module AST : sig ... end

val __TODO_pat__ : Base.String.t -> AST.pat

val __TODO_ty__ : Base.String.t -> AST.ty

val __TODO_term__ : Base.String.t -> AST.term

val __TODO_item__ : Base.String.t -> AST.decl

val int_size_to_string : AST.int_size -> Base.string

val ty_to_string : AST.ty -> Base.string * Base.bool

val ty_to_string_with_paren : AST.ty -> Base.string

val ty_to_string_without_paren : AST.ty -> Base.string

val literal_to_string : AST.literal -> Base.string

val pat_to_string : AST.pat -> Base.bool -> Base__Int.t -> Base.string

val tick_if : Base.bool -> Base.String.t

val term_to_string : AST.term -> Base__Int.t -> Base.string * Base.bool

val term_to_string_with_paren : AST.term -> Base__Int.t -> Base.string

val term_to_string_without_paren : AST.term -> Base__Int.t -> Base.string

val format_to_string : 
  Base.string Base.list ->
  Base.string Base.List.t ->
  Base.string

val term_list_to_string : AST.term Base.list -> Base__Int.t -> Base.string

val decl_to_string : AST.decl -> Base.string

val definition_value_to_equation_definition : 
  AST.definition_type ->
  Base.String.t

val definition_value_to_shell_string : 
  AST.definition_type ->
  Base.String.t ->
  Base.string

val definition_value_to_string : AST.definition_type -> Base.string

val fail_next_obligation : Base.string

val params_to_string_typed : AST.argument Base.list -> Base.string

val params_to_string : (AST.pat * AST.ty) Base.List.t -> Base.string

val inductive_case_args_to_string : 
  AST.inductive_case Base.list ->
  Base.String.t ->
  Base.String.t ->
  Base.String.t ->
  Base.string

val variants_to_string : 
  AST.record_field Base.list ->
  Base.string ->
  Base.String.t ->
  Base.string