Check-in [caa7fbdd73]

Not logged in

Overview
Comment: Added screen shot of the proof assistant, starting a proof. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | trunk files | file ages | folders caa7fbdd73265ada6bb170a4871b156b529268ce 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

Changes to report/arend-report.tex.

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