equal
deleted
inserted
replaced
37 (*defining the abstract constants*) |
37 (*defining the abstract constants*) |
38 |
38 |
39 UU_lift_def "UU_lift == Abs_Lift(Inl(UU))" |
39 UU_lift_def "UU_lift == Abs_Lift(Inl(UU))" |
40 Iup_def "Iup(x) == Abs_Lift(Inr(x))" |
40 Iup_def "Iup(x) == Abs_Lift(Inr(x))" |
41 |
41 |
42 Ilift_def "Ilift(f)(x)== \ |
42 Ilift_def "Ilift(f)(x)== |
43 \ case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f[z]" |
43 case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f[z]" |
44 |
44 |
45 less_lift_def "less_lift(x1)(x2) == \ |
45 less_lift_def "less_lift(x1)(x2) == |
46 \ (case Rep_Lift(x1) of \ |
46 (case Rep_Lift(x1) of |
47 \ Inl(y1) => True \ |
47 Inl(y1) => True |
48 \ | Inr(y2) => \ |
48 | Inr(y2) => |
49 \ (case Rep_Lift(x2) of Inl(z1) => False \ |
49 (case Rep_Lift(x2) of Inl(z1) => False |
50 \ | Inr(z2) => y2<<z2))" |
50 | Inr(z2) => y2<<z2))" |
51 |
51 |
52 end |
52 end |
53 |
53 |
54 |
54 |
55 |
55 |