Check-in [f21f15e5e4]

Not logged in

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

Overview
Comment:Fixed a bug in finding the subproofs of a case-type proof.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:f21f15e5e4a7ad92a584c1360449f7b647264a29
User & Date: andy 2015-04-15 21:38:16
Context
2015-04-16
21:59
Fixed a few bugs in rendering of proofs (commas between antecedants, tabindexes on conclusions so they can be keyboard-focused). check-in: 5ae5431e8f user: andy tags: trunk
2015-04-15
21:38
Fixed a bug in finding the subproofs of a case-type proof. check-in: f21f15e5e4 user: andy tags: trunk
21:37
Updated to use the new inductive (vertical-bar) goal encoding. check-in: 5f036d068a user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to src/proof.js.

35
36
37
38
39
40
41
42
43
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
73
74
75


/* proof.getSubProofs(t)
 * Get the JS array of subproofs from a given proof. Note that this is *child*
 * proofs, not descedants.
 */
proof.getSubProofs = function(t) {
    var proof = t.body[3];
    switch(proof.head) {
        // 0 subproofs
        case "trivial":
        case "hole":
        case "unify":
        case "ctxmem":
            return [];

        // 1 subproof, first argument
        case "ih":
        case "generic":
        case "implies":
        case "backchain":
            return [proof.body[0]];

        // 1 subproof, last argument
        case "induction":
        case "instan":
        case "choice":
            return [proof.body[proof.body.length-1]];

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

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


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







|
|












|





|



|




|




35
36
37
38
39
40
41
42
43
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
73
74
75


/* proof.getSubProofs(t)
 * Get the JS array of subproofs from a given proof. Note that this is *child*
 * proofs, not descedants.
 */
proof.getSubProofs = function(t) {
    var pr = t.body[3];
    switch(pr.head) {
        // 0 subproofs
        case "trivial":
        case "hole":
        case "unify":
        case "ctxmem":
            return [];

        // 1 subproof, first argument
        case "ih":
        case "generic":
        case "implies":
        case "backchain":
            return [pr.body[0]];

        // 1 subproof, last argument
        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));