module Macro_expander:sig
..end
type
level =
| |
Top_level |
| |
Nested |
type
pat_pos =
| |
Bind |
| |
Param |
type
macro_context =
| |
Ctxt_theorem |
| |
Ctxt_other |
typepat_position =
level * pat_pos
module Expander:
val list_to_mac : (macro_context -> 'a -> 'b option) list ->
macro_context -> 'a -> 'b option
val list_to_bool_mac : (pat_position ->
macro_context -> 'a -> 'b option)
list ->
pat_position ->
macro_context -> 'a -> 'b option