exception ConstructorExpected of Term.lsymbol * Ty.tyexception NonExhaustive of Term.pattern listval compile :
get_constructors:(Ty.tysymbol -> Term.lsymbol list) ->
mk_case:(Term.term -> (Term.pattern * 'a) list -> 'a) ->
mk_let:(Term.vsymbol -> Term.term -> 'a -> 'a) ->
Term.term list ->
(Term.pattern list * 'a) list ->
'aval compile_bare :
mk_case:(Term.term -> (Term.pattern * 'a) list -> 'a) ->
mk_let:(Term.vsymbol -> Term.term -> 'a -> 'a) ->
Term.term list ->
(Term.pattern list * 'a) list ->
'aval check_compile :
get_constructors:(Ty.tysymbol -> Term.lsymbol list) ->
Term.term list ->
Term.pattern list list ->
unitval is_exhaustive : Term.term list -> Term.pattern list list -> bool