equal
deleted
inserted
replaced
29 residuals(u2,v2,w2); b:bool|]==> |
29 residuals(u2,v2,w2); b:bool|]==> |
30 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)" |
30 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)" |
31 type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks" |
31 type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks" |
32 |
32 |
33 rules |
33 rules |
34 res_func_def "u |> v == THE w.residuals(u,v,w)" |
34 res_func_def "u |> v == THE w. residuals(u,v,w)" |
35 end |
35 end |
36 |
36 |