IsSumRep
| |
is_sum_rep_def
| inl inr outl outr isl isr |
|  x1 x2 y1 y2 z |
|  IsSumRep (inl x1) |
|  IsSumRep (inr y1) |
|  (IsSumRep z |
|  inl (outl z) = z inr (outr z) = z) |
|  (inl x1 = inl x2 x1 = x2) |
|  (inr y1 = inr y2 y1 = y2) |
|  inl x1 = inr y1 |
|  inr y1 = inl x1 |
|  outl (inl x1) = x1 |
|  outr (inr y1) = y1 |
|  (IsSumRep z (isl z inl (outl z) = z)) |
|  (IsSumRep z (isr z inr (outr z) = z)) |
+
| |
sum_def | f TypeDefn IsSumRep f |
InL
| |
InR
| |
OutL
| |
OutR
| |
IsL
| |
IsR
| |
sum_clauses
| x1 x2 y1 y2 z |
|  (InL (OutL z) = z InR (OutR z) = z) |
|  (InL x1 = InL x2 x1 = x2) |
|  (InR y1 = InR y2 y1 = y2) |
|  InL x1 = InR y1 |
|  InR y1 = InL x1 |
|  OutL (InL x1) = x1 |
|  OutR (InR y1) = y1 |
|  (IsL z InL (OutL z) = z) |
|  (IsR z InR (OutR z) = z) |