Check-in [626e89a1ac]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fixed client-side proof handling to work with the new backchain fomat.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | bc-subst
Files: files | file ages | folders
SHA1:626e89a1acf8628e35d96f2e9ef4371189690496
User & Date: andy 2015-04-21 15:47:00
Context
2015-04-21
15:47
Fixed module imports to avoid a (meaningless) warning. check-in: 8ad421112c user: andy tags: bc-subst
15:47
Fixed client-side proof handling to work with the new backchain fomat. check-in: 626e89a1ac user: andy tags: bc-subst
15:46
Added support for showing rule names in derivations. check-in: a989ccc9e5 user: andy tags: bc-subst
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to src/proof.js.

44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

66
67
68





69
70
71
72
        // 0 subproofs
        case "trivial":
        case "hole":
        case "unify":
        case "ctxmem":
            return [];

        // 1 subproof, always in the last argument.
        case "ih":
        case "generic":
        case "implies":
        case "backchain":
        case "induction":
        case "instan":
        case "choice":
            return [pr.body[pr.body.length-1]];

        // Product
        case "product":
            return terms.toArray(pr.body[0]);
    }


    // The only other option is case, which always has a list of
    // subproofs (0,1, or N elements):
    return terms.toArray(pr.body[3]);





}


}(typeof exports === 'undefined' ? (this['arend']['proof'] = {}) : exports));







<
<
<
<
<
<
<
<
<
<



|
<
>
|
<
|
>
>
>
>
>




44
45
46
47
48
49
50










51
52
53
54

55
56

57
58
59
60
61
62
63
64
65
66
        // 0 subproofs
        case "trivial":
        case "hole":
        case "unify":
        case "ctxmem":
            return [];











        // Product
        case "product":
            return terms.toArray(pr.body[0]);


        // Case always has a list of subproofs in its fourth argument
        case "case":

            return terms.toArray(pr.body[3]);

        // Everything else has a single subproof, in its last argument
        default:
            return [pr.body[pr.body.length-1]];
    }
}


}(typeof exports === 'undefined' ? (this['arend']['proof'] = {}) : exports));