| changeset 20647 | 680b58597f65 |
| 20646:02729d4d6e4a | 20647:680b58597f65 |
|---|---|
1 %ID: $Id$ |
|
2 %Author: Jia Meng, NICTA |
|
3 %full-typed combinator reduction for I, K |
|
4 |
|
5 %K P Q --> P |
|
6 input_clause(a1,axiom, |
|
7 [++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(P,A)),tc_fun(B,A)),typeinfo(Q,B)),A),typeinfo(P,A))]). |
|
8 |
|
9 %I P --> P |
|
10 input_clause(a3,axiom, |
|
11 [++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]). |