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 Side-by-Side Diffs Ignore Whitespace Patch

Changes to src/term_render.js.

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