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