>> Inspector Lestrade says: >> Welcome to the Lestrade Type Inspector, >> full solution to name collisions >> (renames identifiers in saved or imported moves). >> matching of lambda terms installed, not sure how to test it >> interface refinements >> disabled prop/type symmetry re rewrite feature >> version of 12/2/2016 >> 7 pm Boise time declare x obj >> x: obj {move 1} declare y obj >> y: obj {move 1} construct pair x y obj >> pair: [(x_1:obj),(y_1:obj) => (---:obj)] >> {move 0} construct p1 x obj >> p1: [(x_1:obj) => (---:obj)] >> {move 0} construct p2 x obj >> p2: [(x_1:obj) => (---:obj)] >> {move 0} rewritec First x y p1 pair x y, x >> u: that P(p1((x pair y))) {move 1} >> First: [(x_1:obj),(y_1:obj),(P_1:[(x1_2:obj) >> => (---:prop)]), >> (u_1:that P_1(p1((x_1 pair y_1)))) => >> (---:that P_1(x_1))] >> {move 0} rewritec Second x y p2 pair x y, y >> v: that P(p2((x pair y))) {move 1} >> Second: [(x_1:obj),(y_1:obj),(P_1:[(x1_2: >> obj) => (---:prop)]), >> (v_1:that P_1(p2((x_1 pair y_1)))) => >> (---:that P_1(y_1))] >> {move 0} open declare x1 obj >> x1: obj {move 2} declare y1 obj >> y1: obj {move 2} define reverse x1 : pair (p2 x1, p1 x1) >> reverse: [(x1_1:obj) => ((p2(x1_1) pair >> p1(x1_1)):obj)] >> {move 1} define reversetest x1 y1 : reverse (pair x1 y1) >> reversetest: [(x1_1:obj),(y1_1:obj) >> => (reverse((x1_1 pair y1_1)):obj)] >> {move 1} close % notice that Lestrade executes the pair reversal! define testing x y: reversetest x y >> testing: [(x_1:obj),(y_1:obj) => ((y_1 pair >> x_1):obj)] >> {move 0} clearcurrent % associative law simplication % I believe I have implemented almost the full power of the Watson % rewrite rule programming scheme. The interlock between matching and % rewriting should make it possible to implement its control structures % without extra primitives. construct Nat type >> Nat: type {move 0} declare m in Nat >> m: in Nat {move 1} declare n in Nat >> n: in Nat {move 1} declare p in Nat >> p: in Nat {move 1} construct + m n in Nat >> +: [(m_1:in Nat),(n_1:in Nat) => (---:in >> Nat)] >> {move 0} construct assoc m in Nat >> assoc: [(m_1:in Nat) => (---:in Nat)] >> {move 0} construct assocs m in Nat >> assocs: [(m_1:in Nat) => (---:in Nat)] >> {move 0} rewritec Assocfails m assoc m, m >> u: that Pn(assoc(m)) {move 1} >> Assocfails: [(m_1:in Nat),(Pn_1:[(m1_2:in >> Nat) => (---:prop)]), >> (u_1:that Pn_1(assoc(m_1))) => (---: >> that Pn_1(m_1))] >> {move 0} rewritec Assocsfails m assocs m, m >> v: that Pn(assocs(m)) {move 1} >> Assocsfails: [(m_1:in Nat),(Pn_1:[(m1_2:in >> Nat) => (---:prop)]), >> (v_1:that Pn_1(assocs(m_1))) => (---: >> that Pn_1(m_1))] >> {move 0} rewritec Assocrule m n p (m + n) + p, m + (n + p) >> w: that Pn(((m + n) + p)) {move 1} >> Assocrule: [(m_1:in Nat),(n_1:in Nat),(p_1: >> in Nat),(Pn_1:[(m1_2:in Nat) => (---: >> prop)]), >> (w_1:that Pn_1(((m_1 + n_1) + p_1))) >> => (---:that Pn_1((m_1 + (n_1 + p_1))))] >> {move 0} rewritec Assocsrule m n p (m + n) + p, assocs(assoc(m + (assocs (n+p)))) >> x: that Pn(((m + n) + p)) {move 1} >> Assocsrule: [(m_1:in Nat),(n_1:in Nat),(p_1: >> in Nat),(Pn_1:[(m1_2:in Nat) => (---: >> prop)]), >> (x_1:that Pn_1(((m_1 + n_1) + p_1))) >> => (---:that Pn_1(assocs(assoc((m_1 >> + assocs((n_1 + p_1)))))))] >> {move 0} declare q in Nat >> q: in Nat {move 1} define test m n p q:(m+n)+(p+q) >> test: [(m_1:in Nat),(n_1:in Nat),(p_1:in >> Nat),(q_1:in Nat) => ((m_1 + (n_1 + >> (p_1 + q_1))):in Nat)] >> {move 0} declare r in Nat >> r: in Nat {move 1} declare s in Nat >> s: in Nat {move 1} define test2 m n p q r s:((m+n)+p)+((q+r)+s) >> test2: [(m_1:in Nat),(n_1:in Nat),(p_1:in >> Nat),(q_1:in Nat),(r_1:in Nat),(s_1: >> in Nat) => ((m_1 + (n_1 + (p_1 + (q_1 >> + (r_1 + s_1))))):in Nat)] >> {move 0} clearcurrent declare x in Nat >> x: in Nat {move 1} declare y in Nat >> y: in Nat {move 1} construct * x y : in Nat >> *: [(x_1:in Nat),(y_1:in Nat) => (---:in >> Nat)] >> {move 0} construct 2 : in Nat >> 2: in Nat {move 0} rewritec Double x x+x, 2*x >> zzz: that Pn((x + x)) {move 1} >> Double: [(x_1:in Nat),(Pn_1:[(x1_2:in Nat) >> => (---:prop)]), >> (zzz_1:that Pn_1((x_1 + x_1))) => (---: >> that Pn_1((2 * x_1)))] >> {move 0} construct 1 in Nat >> 1: in Nat {move 0} define 3:1+2 >> 3: [((1 + 2):in Nat)] >> {move 0} define 6: 3+(1+2) >> 6: [((2 * 3):in Nat)] >> {move 0} define six:(1+2)+3 >> six: [((2 * (1 + 2)):in Nat)] >> {move 0} >> Inspector Lestrade says: Done reading scratch to rewrites: >> type lines or type quit to exit interface quit