sig
  type level = Top_level | Nested
  type pat_pos = Bind | Param
  type macro_context = Ctxt_theorem | Ctxt_other
  type pat_position = Macro_expander.level * Macro_expander.pat_pos
  module Expander :
    functor (C : Typed_ast.Exp_context) ->
      sig
        val expand_defs :
          Typed_ast.def list ->
          (Macro_expander.macro_context ->
           Typed_ast.exp -> Typed_ast.exp option) *
          (Types.t -> Types.t) * (Types.src_t -> Types.src_t) *
          (Macro_expander.pat_position ->
           Macro_expander.macro_context ->
           Typed_ast.pat -> Typed_ast.pat option) ->
          Typed_ast.def list
        val expand_pat :
          Macro_expander.macro_context ->
          Macro_expander.pat_position ->
          Typed_ast.pat ->
          (Types.t -> Types.t) * (Types.src_t -> Types.src_t) *
          (Macro_expander.pat_position ->
           Macro_expander.macro_context ->
           Typed_ast.pat -> Typed_ast.pat option) ->
          Typed_ast.pat
        val expand_exp :
          Macro_expander.macro_context ->
          (Macro_expander.macro_context ->
           Typed_ast.exp -> Typed_ast.exp option) *
          (Types.t -> Types.t) * (Types.src_t -> Types.src_t) *
          (Macro_expander.pat_position ->
           Macro_expander.macro_context ->
           Typed_ast.pat -> Typed_ast.pat option) ->
          Typed_ast.exp -> Typed_ast.exp
      end
  val list_to_mac :
    (Macro_expander.macro_context -> 'a -> 'b option) list ->
    Macro_expander.macro_context -> 'a -> 'b option
  val list_to_bool_mac :
    (Macro_expander.pat_position ->
     Macro_expander.macro_context -> 'a -> 'b option)
    list ->
    Macro_expander.pat_position ->
    Macro_expander.macro_context -> 'a -> 'b option
end