Check-in [a989ccc9e5]

Not logged in

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

Overview
Comment:Added support for showing rule names in derivations.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | bc-subst
Files: files | file ages | folders
SHA1:a989ccc9e5f2e15c85831663b8c3cf1814885ac9
User & Date: andy 2015-04-21 15:46:20
Context
2015-04-21
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
15:45
Fixed a bug in the translation of Uppercase atoms from Prolog. check-in: 223107a48f user: andy tags: bc-subst
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to src/term_render.js.

278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
                        induction : "By induction",
                        ih : "IH",
                        generic : "∀-R",
                        instan : "∃-R",
                        product : "∧-R",
                        choice : "∨-R",
                        implies : "→R",
                        backchain : "", 
                    }[name];
                else 
                    return {
                        false_left : "⊥-L",
                        and_left : "∧-L",
                        or_left : "∨-L",
                        forall_left : "∀-L",







|







278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
                        induction : "By induction",
                        ih : "IH",
                        generic : "∀-R",
                        instan : "∃-R",
                        product : "∧-R",
                        choice : "∨-R",
                        implies : "→R",
                        backchain : proof.body[3].body[0], 
                    }[name];
                else 
                    return {
                        false_left : "⊥-L",
                        and_left : "∧-L",
                        or_left : "∨-L",
                        forall_left : "∀-L",