Check-in [caa7fbdd73]

Not logged in

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

Overview
Comment:Added screen shot of the proof assistant, starting a proof.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:caa7fbdd73265ada6bb170a4871b156b529268ce
User & Date: andy 2015-04-15 11:44:40
Context
2015-04-15
11:47
Split the `What` argument to elaborate into `What` and `Data`. What is now either 'goal' or 'ctx', while data identifies the sub-element. For ctx this is the index, but it can also be the index of a disjunct (when the goal is a disjunction), or 'ih' to indicate backchaining the user goal on the IH instead of on its definitions. check-in: 9e954b6b56 user: andy tags: trunk
11:44
Added screen shot of the proof assistant, starting a proof. check-in: caa7fbdd73 user: andy tags: trunk
11:12
Added some utilities for working with proof terms (extracting subproofs, getting proof goals, navigating through proofs on a path, etc.) check-in: e902cf4ec5 user: andy tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to report/arend-report.tex.

   959    959   \includegraphics[width=6.5in]{repl-sample.png}
   960    960   \end{centering}
   961    961   
   962    962   \caption{The browser-based run-eval-print-loop interface}
   963    963   \label{fig:repl}
   964    964   \end{figure*}
   965    965   
          966  +
          967  +\begin{figure*}[ht!]
          968  +
          969  +\begin{centering}
          970  +\includegraphics[width=6.5in]{proof-start-sample.png}
          971  +\end{centering}
          972  +
          973  +\caption{The proof assistant interface, with an incomplete inductive proof}
          974  +\label{fig:passist1}
          975  +\end{figure*}
          976  +
   966    977   
   967    978   \clearpage
   968    979   \section{Implementation}
   969    980   
   970    981   \newthought{Arend currently exists} in two semi-overlapping implementations:
   971    982   \begin{itemize}
   972    983   \item A \emph{client-based} implementation, written in JavaScript and running

Added report/proof-start-sample.png.

cannot compute difference between binary files