1signature sumSyntax =
2sig
3  include Abbrev
4
5  val inl_tm : term
6  val inr_tm : term
7  val isl_tm : term
8  val isr_tm : term
9  val outl_tm : term
10  val outr_tm : term
11  val sum_case_tm : term
12
13  val mk_sum      : hol_type * hol_type -> hol_type
14  val dest_sum    : hol_type -> hol_type * hol_type
15  val strip_sum   : hol_type -> hol_type list
16  val list_mk_sum : hol_type list -> hol_type
17
18  val mk_inl      : term * hol_type -> term
19  val mk_inr      : term * hol_type -> term
20  val mk_isl      : term -> term
21  val mk_isr      : term -> term
22  val mk_outl     : term -> term
23  val mk_outr     : term -> term
24  val mk_sum_case : term * term * term -> term
25
26  val dest_inl  : term -> term * hol_type
27  val dest_inr  : term -> term * hol_type
28  val dest_isl  : term -> term
29  val dest_isr  : term -> term
30  val dest_outl : term -> term
31  val dest_outr : term -> term
32
33  val is_inl  : term -> bool
34  val is_inr  : term -> bool
35  val is_isl  : term -> bool
36  val is_isr  : term -> bool
37  val is_outl : term -> bool
38  val is_outr : term -> bool
39
40  datatype ('a, 'b) sum = INL of 'a | INR of 'b
41
42  val lift_sum    : hol_type -> ('a -> term )
43                             -> ('b -> term)
44                             -> ('a,'b)sum
45                             -> term
46end
47